Abstract
We present models and soundness results for hybrid information flow, i.e. for mechanisms that enforce noninterference-style security guarantees using a combination of static analysis and dynamic taint tracking. Our analysis has the following characteristics: (i) we formulate hybrid information flow as an end-to-end property, in contrast to disruptive monitors that prematurely terminate or otherwise alter an execution upon detecting a potentially illicit flow; (ii) our security notions capture the increased precision that is gained when static analysis is combined with dynamic enforcement; (iii) we introduce path tracking to incorporate a form of termination-sensitivity, and (iv) develop a novel variant of purely dynamic tracking that ignores indirect flows; (v) our work has been formally verified, by a comprehensive representation in the theorem prover Coq.
This work was funded in part by the Air Force Office of Scientific Research (FA9550-09-1-0138).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Amtoft, T., Dodds, J., Zhang, Z., Appel, A., Beringer, L., Hatcliff, J., Ou, X., Cousino, A.: A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol. 7215, pp. 369–389. Springer, Heidelberg (2012)
Appel, A.W.: Verified software toolchain - (invited talk). In: Barthe (ed.) [6], pp. 1–17
Austin, T.H., Flanagan, C.: Efficient purely-dynamic information flow analysis. In: Chong, S., Naumann, D. (eds.) PLAS 2009: Proceedings of the 4th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, pp. 113–124. ACM (2009)
Austin, T.H., Flanagan, C.: Permissive dynamic information flow analysis. In: Banerjee, A., Garg, D. (eds.) PLAS 2010: Proceedings of the 5th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, pp. 3:1–3:12. ACM (2010)
Austin, T.H., Flanagan, C., Abadi, M.: A functional view of imperative information flow. Technical Report UCSC-SOE-12-15, Department of Computer Science, University of California at Santa Cruz (2012)
Barthe, G. (ed.): ESOP 2011. LNCS, vol. 6602. Springer, Heidelberg (2011)
Barthe, G., Pichardie, D., Rezk, T.: A Certified Lightweight Non-interference Java Bytecode Verifier. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 125–140. Springer, Heidelberg (2007)
Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Jones, N.D., Leroy, X. (eds.) Proceedings of the 31st ACM Symposium on Principles of Programming Languages, POPL 2004, pp. 14–25. ACM (2004)
Beringer, L.: End-to-end multilevel hybrid information flow control - Coq development (2012), http://www.cs.princeton.edu/~eberinge/HybridIFC.tar.gz
Beringer, L., Hofmann, M.: Secure information flow and program logics. In: Proceedings of the 20th IEEE Computer Security Foundations Symposium, CSF 2007, pp. 233–248. IEEE Computer Society (2007)
Boudol, G.: On Typing Information Flow. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 366–380. Springer, Heidelberg (2005)
Boudol, G.: Secure Information Flow as a Safety Property. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 20–34. Springer, Heidelberg (2009)
Chudnov, A., Naumann, D.A.: Information flow monitor inlining. In: CSF 2010 [15], pp. 200–214 (2010)
Clause, J.A., Li, W., Orso, A.: Dytan: a generic dynamic taint analysis framework. In: Rosenblum, D.S., Elbaum, S.G. (eds.) Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2007, pp. 196–206. ACM (2007)
Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010. IEEE Computer Society (2010)
Hunt, S., Sands, D.: On flow-sensitive security types. In: Morrisett, J.G., Jones, S.L.P. (eds.) Proceedings of the 33rd ACM Symposium on Principles of Programming Languages, POPL 2006, pp. 79–90. ACM (2006)
Hunt, S., Sands, D.: From exponential to polynomial-time security typing via principal types. In: Barthe (ed.) [6], pp. 297–316
Jee, K., Portokalidis, G., Kemerlis, V.P., Ghosh, S., August, D.I., Keromytis, A.D.: A general approach for efficiently accelerating software-based dynamic data flow tracking on commodity hardware. In: Proceedings of the 19th Network and Distributed System Security Symposium, NDSS 2012. The Internet Society, ISOC (2012)
Kang, M.G., McCamant, S., Poosankam, P., Song, D.: DTA++: Dynamic taint analysis with targeted control-flow propagation. In: Proceedings of the 18th Network and Distributed System Security Symposium, NDSS 2011. The Internet Society, ISOC (2011)
Le Guernic, G.: Precise Dynamic Verification of Confidentiality. In: Beckert, B., Klein, G. (eds.) Proceedings of the 5th International Verification Workshop. CEUR Workshop Proceedings, vol. 372, pp. 82–96. CEUR-WS.org (2008)
Le Guernic, G., Jensen, T.: Monitoring Information Flow. In: Sabelfeld, A. (ed.) Proceedings of the Workshop on Foundations of Computer Security, FCS 2005, pp. 19–30. DePaul University (June 2005) (Affiliated with LICS 2005)
Magazinius, J., Russo, A., Sabelfeld, A.: On-the-fly Inlining of Dynamic Security Monitors. In: Rannenberg, K., Varadharajan, V., Weber, C. (eds.) SEC 2010. IFIP AICT, vol. 330, pp. 173–186. Springer, Heidelberg (2010)
Masri, W., Podgurski, A., Leon, D.: Detecting and debugging insecure information flows. In: Proceedings of the 15th International Symposium on Software Reliability Engineering, ISSRE 2004, pp. 198–209. IEEE Computer Society (2004)
Moore, S., Chong, S.: Static analysis for efficient hybrid information-flow control. In: Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, pp. 146–160. IEEE Computer Society (2011)
Nanevski, A., Banerjee, A., Garg, D.: Verification of information flow and access control policies with dependent types. In: 32nd IEEE Symposium on Security and Privacy, S&P 2011, pp. 165–179. IEEE Computer Society (2011)
Rangan, R., Vachharajani, N., Vachharajani, M., August, D.I.: Decoupled software pipelining with the synchronization array. In: Proceedings of the 13th International Conference on Parallel Architectures and Compilation Techniques, PACT 2004, pp. 177–188. IEEE Computer Society (2004)
Russo, A., Sabelfeld, A.: Dynamic vs. static flow-sensitive security analysis. In: CSF 2010 [15], pp. 186–199 (2010)
Sabelfeld, A., Russo, A.: From Dynamic to Static and Back: Riding the Roller Coaster of Information-Flow Control Research. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 352–365. Springer, Heidelberg (2010)
Vachharajani, N., Bridges, M.J., Chang, J., Rangan, R., Ottoni, G., Blome, J.A., Reis, G.A., Vachharajani, M., August, D.I.: Rifle: An architectural framework for user-centric information-flow security. In: 37th Annual International Symposium on Microarchitecture (MICRO-37), pp. 243–254. IEEE Computer Society (2004)
Venkatakrishnan, V.N., Xu, W., DuVarney, D.C., Sekar, R.: Provably Correct Runtime Enforcement of Non-interference Properties. In: Ning, P., Qing, S., Li, N. (eds.) ICICS 2006. LNCS, vol. 4307, pp. 332–351. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beringer, L. (2012). End-to-end Multilevel Hybrid Information Flow Control. In: Jhala, R., Igarashi, A. (eds) Programming Languages and Systems. APLAS 2012. Lecture Notes in Computer Science, vol 7705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35182-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-35182-2_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35181-5
Online ISBN: 978-3-642-35182-2
eBook Packages: Computer ScienceComputer Science (R0)