Abstract
We present the current state of the art of information flow analyses for Go applications. Based on our findings, we discuss future directions of where static analysis information can be used at runtime to for example achieve higher precision, or optimise runtime checks. We focus specifically on outstanding language features such as closures and message-based communication via channels.
The work was partially supported by the Norwegian-German bilateral PPP project GoRETech (GoRuntime Enforcement Techniques), the EU COST Action IC1402 “ARVI—Runtime Verification Beyond Monitoring” and the EU project FP7-610582 Envisage: Engineering Virtualized Services.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Andrews, G.R., Reitman, R.P.: An axiomatic approach to information flow in programs. ACM Trans. Program. Lang. Syst. 2(1), 56–76 (1980)
Arzt, S., et al.: FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Androidapps. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (2014)
Coffman Jr., E.G., Elphick, M., Shoshani, A.: System deadlocks. Comput. Surv. 3(2), 67–78 (1971)
Cytron, R., et al.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991)
Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976)
Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977)
Donovan, A.A.A., Kernighan, B.W.: The Go Programming Language (2015)
Effective Go - The Go Programming Language. https://golang.org/doc/effective_go.html#concurrency. Accessed 29 Apr 2016
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)
Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)
Kobayashi, N.: Type-based information flow analysis for the \(\pi \)-calculus. Acta Informatica 42(4), 291–347 (2005)
Laddad, R.: AspectJ in Action: Practical Aspect-Oriented Programming. Manning Publications Co., Greenwich (2003)
Livshits, B., Chong, S.: Towards fully automatic placement of security sanitizers and declassifiers. In: The 40th Annual ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 385–398. ACM (2013)
Livshits, V.B., Lam, M.S.: Finding security vulnerabilities in Java applications with static analysis. In: Proceedings of the 14th Conference on USENIX Security Symposium. SSYM 2005. USENIX Association (2005)
Livshits, V.B., Lam, M.S.: Tracking pointers with path and context sensitivity for bug detection in C programs. In: Proceedings of the 9th European Software Engineering Conference. ESEC/FSE-11, pp. 317–326. ACM (2003)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Part I/II. Inf. Comput. 100, 1–77 (1992)
Myers, A.C.: JFlow: practical mostly-static information flow control. In: Proceedings of the 26th ACM Symposium on Principles of Programming Languages, pp. 228–241 (1999)
Nielson, F., Nielson, H.-R., Hankin, C.L.: Principles of Program Analysis. Springer, Heidelberg (1999)
Padhye, R., Khedker, U.P.: Interprocedural data flow analysis in SOOT using value contexts. In: Proceedings of the 2nd ACM SIGPLAN International Workshop on State of the Art in Java Program Analysis. ACM (2013)
Pistoia, M., Flynn, R.J., Koved, L., Sreedhar, V.C.: Interprocedural analysis for privileged code placement and tainted variable detection. In: Gao, X.-X. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 362–386. Springer, Heidelberg (2005)
Pottier, F., Simonet, V.: Information flow inference for ML. ACM Trans. Program. Lang. Syst. 25(1), 117–158 (2003)
Schwartz, E.J., Avgerinos, T., Brumley, D.: All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask). In: 2010 IEEE Symposium on Security and Privacy (SP), pp. 317–331. IEEE (2010)
Steffen, M.: A small-step semantics of a concurrent calculus with goroutines and deferred functions. In: Abraham, E., Bonsangue, M., Johnsen, E.B. (eds.) Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. LNCS, vol. 9660, pp. 393–406. Springer, Heidelberg (2016)
Stolz, V., Bodden, E.: Temporal assertions using AspectJ. Electron. Notes Theor. Comput. Sci. 144(4), 109–124 (2006)
Summerfield, M.: Programming in Go (2012)
The cover story - The Go Blog. https://blog.golang.org/cover. Accessed 29 Apr 2016
Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2–3), 167–187 (1996)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Bodden, E., Pun, K.I., Steffen, M., Stolz, V., Wickert, AK. (2016). Information Flow Analysis for Go. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. ISoLA 2016. Lecture Notes in Computer Science(), vol 9952. Springer, Cham. https://doi.org/10.1007/978-3-319-47166-2_30
Download citation
DOI: https://doi.org/10.1007/978-3-319-47166-2_30
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47165-5
Online ISBN: 978-3-319-47166-2
eBook Packages: Computer ScienceComputer Science (R0)