Hostname: page-component-8448b6f56d-c4f8m Total loading time: 0 Render date: 2024-04-25T01:12:25.478Z Has data issue: false hasContentIssue false
  • English
  • Français

Testing noninterference, quickly

Part of: JFP Research Articles

Published online by Cambridge University Press:  05 April 2016

CĂTĂLIN HRIŢCU ,
LEONIDAS LAMPROPOULOS ,
ANTAL SPECTOR-ZABUSKY ,
ARTHUR AZEVEDO DE AMORIM ,
MAXIME DÉNÈS ,
JOHN HUGHES ,
BENJAMIN C. PIERCE  and
DIMITRIOS VYTINIOTIS
CĂTĂLIN HRIŢCU
Affiliation:
Inria Paris, Prosecco team, Paris, France (e-mail: catalin.hritcu@inria.fr)
LEONIDAS LAMPROPOULOS
Affiliation:
Department of Computer and Information Science, University of Pennsylvania, Philadelphia, USA
ANTAL SPECTOR-ZABUSKY
Affiliation:
Department of Computer and Information Science, University of Pennsylvania, Philadelphia, USA
ARTHUR AZEVEDO DE AMORIM
Affiliation:
Department of Computer and Information Science, University of Pennsylvania, Philadelphia, USA
MAXIME DÉNÈS
Affiliation:
Inria Paris, Gallium team, Paris, France
JOHN HUGHES
Affiliation:
Computer Science and Engineering, Chalmers University, Gothenburg, Sweden
BENJAMIN C. PIERCE
Affiliation:
Department of Computer and Information Science, University of Pennsylvania, Philadelphia, USA
DIMITRIOS VYTINIOTIS
Affiliation:
Programming Principles and Tools group, Microsoft Research, Cambridge, UK
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Information-flow control mechanisms are difficult both to design and to prove correct. To reduce the time wasted on doomed proof attempts due to broken definitions, we advocate modern random-testing techniques for finding counterexamples during the design process. We show how to use QuickCheck, a property-based random-testing tool, to guide the design of increasingly complex information-flow abstract machines, leading up to a sophisticated register machine with a novel and highly permissive flow-sensitive dynamic enforcement mechanism that is sound in the presence of first-class public labels. We find that both sophisticated strategies for generating well-distributed random programs and readily falsifiable formulations of noninterference properties are critically important for efficient testing. We propose several approaches and evaluate their effectiveness on a collection of injected bugs of varying subtlety. We also present an effective technique for shrinking large counterexamples to minimal, easily comprehensible ones. Taken together, our best methods enable us to quickly and automatically generate simple counterexamples for more than 45 bugs. Moreover, we show how testing guides the discovery of the sophisticated invariants needed for the noninterference proof of our most complex machine.

Type
Articles
Information
Journal of Functional Programming , Volume 26 , 2016 , e4
Copyright
Copyright © Cambridge University Press 2016 

References

Antoy, S. (2000) A needed narrowing strategy. J. ACM 47 (4), 776–822.CrossRefGoogle Scholar
Austin, T. H. & Flanagan, C. (2009) Efficient purely-dynamic information flow analysis. In Proceedings of 4th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, PLAS'09. ACM, pp. 113–124.CrossRefGoogle Scholar
Austin, T. H. & Flanagan, C. (2010) Permissive dynamic information flow analysis. In Proceedings of 5th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, PLAS'10. ACM, pp. 3:1–3:12.CrossRefGoogle Scholar
Azevedo de Amorim, A., Collins, N., DeHon, A., Demange, D., Hriţcu, C., Pichardie, D., Pierce, B. C., Pollack, R. & Tolmach, A. (January 2014) A verified information-flow architecture. In Proceedings of 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'14. ACM, pp. 165–178.CrossRefGoogle Scholar
Azevedo de Amorim, A., Dénès, M., Giannarakis, N., Hriţcu, C., Pierce, B. C., Spector-Zabusky, A. & Tolmach, A. (2015) Micro-policies: Formally verified, tag-based security monitors. In Proceedings of 36th IEEE Symposium on Security and Privacy, SP'15. IEEE, pp. 813–830.CrossRefGoogle Scholar
Balliu, M., Dam, M. & Guernic, G. L. (2012) Encover: Symbolic exploration for information flow security. In Proceedings of 25th IEEE Computer Security Foundations Symposium, CSF'12. IEEE, pp. 30–44.CrossRefGoogle Scholar
Banerjee, A. & Naumann, D. A. (2005) Stack-based access control and secure information flow. J. Funct. Program. 15 (2), 131–177.CrossRefGoogle Scholar
Barthe, G., Crespo, J. M. & Kunz, C. (2011a) Relational verification using product programs. In Proceedings of 17th International Symposium on Formal Methods, FM'11, Lecture Notes in Computer Science, vol. 6664. Springer, pp. 200–214.Google Scholar
Barthe, G., D'Argenio, P. R. & Rezk, T. (2011b) Secure information flow by self-composition. Math. Struct. Comput. Sci. 21 (6), 1207–1252.CrossRefGoogle Scholar
Benton, N. (2004) Simple relational correctness proofs for static analyses and program transformations. In Proceedings of 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'04. ACM, pp. 14–25.CrossRefGoogle Scholar
Berghofer, S. & Nipkow, T. (2004) Random testing in Isabelle/HOL. In Proceedings of 2nd International Conference on Software Engineering and Formal Methods, SEFM'04. IEEE CS, pp. 230–239.CrossRefGoogle Scholar
Bichhawat, A., Rajani, V., Garg, D. & Hammer, C. (2014a) Information flow control in WebKit's JavaScript bytecode. In Proceedings of 3rd International Conference on Principles of Security and Trust, POST'14, Lecture Notes in Computer Science, vol. 8414. Springer, pp. 159–178.Google Scholar
Bichhawat, A., Rajani, V., Garg, D. & Hammer, C. (2014b) Generalizing permissive-upgrade in dynamic information flow analysis. In Proceedings of 9th Workshop on Programming Languages and Analysis for Security, PLAS'14. ACM, pp. 15–24.CrossRefGoogle Scholar
Birgisson, A., Hedin, D. & Sabelfeld, A. (2012) Boosting the permissiveness of dynamic information-flow tracking by testing. In Proceedings of 17th European Symposium on Research in Computer Security, ESORICS'12, Lecture Notes in Computer Science, vol. 7459. Springer, pp. 55–72.CrossRefGoogle Scholar
Buiras, P., Stefan, D., & Russo, A. (2014) On dynamic flow-sensitive floating-label systems. In Proceedings of 27th IEEE Computer Security Foundations Symposium, CSF'14. IEEE, pp. 65–79.CrossRefGoogle Scholar
Bulwahn, L. (2012a) The new Quickcheck for Isabelle - random, exhaustive and symbolic testing under one roof. In Proceedings of 2nd International Conference on Certified Programs and Proofs, CPP'12, Lecture Notes in Computer Science, vol. 7679. Springer, pp. 92–108.Google Scholar
Bulwahn, L. (2012b) Smart testing of functional programs in Isabelle. In Proceedings of 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'12, Lecture Notes in Computer Science, vol. 7180, Springer, pp. 153–167.Google Scholar
Burnim, J. & Sen, K. (2008) Heuristics for scalable dynamic test generation. In Proceedings of 23rd IEEE/ACM International Conference on Automated Software Engineering, ASE'08, IEEE Computer Society, pp. 443–446.CrossRefGoogle Scholar
Cadar, C., Dunbar, D. & Engler, D. (2008) KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of 8th USENIX Conference on Operating Systems Design and Implementation, OSDI'08. USENIX Association, pp. 209–224.Google Scholar
Cadar, C., Ganesh, V., Pawlowski, P. M., Dill, D. L. & Engler, D. R. (2006) EXE: Automatically generating inputs of death. In Proceedings of 13th ACM Conference on Computer and Communications Security, CCS'06. ACM, pp. 322–335.CrossRefGoogle Scholar
Cadar, C., Godefroid, P., Khurshid, S., Păsăreanu, C. S., Sen, K., Tillmann, N. & Visser, W. (2011) Symbolic execution for software testing in practice: preliminary assessment. In Proceedings of 33rd International Conference on Software Engineering, ICSE'11. ACM, pp. 1066–1071.CrossRefGoogle Scholar
Cadar, C. & Sen, K. (2013) Symbolic execution for software testing: Three decades later. Commun. ACM 56 (2), 82–90.CrossRefGoogle Scholar
Chamarthi, H. R., Dillinger, P. C., Kaufmann, M. & Manolios, P. (2011) Integrating testing and interactive theorem proving. In Proceedings of 10th International Workshop on the ACL2 Theorem Prover and its Applications, Electronic Proceedings in Theoretical Computer Science, vol. 70, pp. 4–19. http://www.eptcs.org/ CrossRefGoogle Scholar
Christiansen, J. & Fischer, S. (2008) EasyCheck – test data for free. In Proceedings of 9th International Symposium on Functional and Logic Programming, FLOPS'08, Lecture Notes in Computer Science, vol. 4989. Springer, pp. 322–336.CrossRefGoogle Scholar
Claessen, K., Duregård, J. & Pałka, M. H. (2014) Generating constrained random data with uniform distribution. In Proceedings of 12th International Symposium on Functional and Logic Programming, Lecture Notes in Computer Science, vol. 8475. Springer, pp. 18–34.CrossRefGoogle Scholar
Claessen, K. & Hughes, J. (2000) QuickCheck: A lightweight tool for random testing of Haskell programs. In Proceedings of 5th ACM SIGPLAN International Conference on Functional Programming, ICFP'00. ACM, pp. 268–279.CrossRefGoogle Scholar
Clarkson, M. R. & Schneider, F. B. (2010) Hyperproperties. J. Comput. Secur. 18 (6), 1157–1210.CrossRefGoogle Scholar
Dybjer, P., Haiyan, Q. & Takeyama, M. (2003) Combining testing and proving in dependent type theory. In Proceedings of 16th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'03, Lecture Notes in Computer Science, vol. 2758. Springer, pp. 188–203.CrossRefGoogle Scholar
Eastlund, C. (2009) DoubleCheck your theorems. In Proceedings of 8th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2'09. ACM, pp. 42–46.CrossRefGoogle Scholar
Fenton, J. S. (1974) Memoryless subsystems. Comput. J. 17 (2), 143–147.CrossRefGoogle Scholar
Fetscher, B., Claessen, K., Palka, M. H., Hughes, J. & Findler, R. B. (2015) Making random judgments: Automatically generating well-typed terms from the definition of a type-system. In Proceedings of 24th European Symposium on Programming, ESOP'15, Lecture Notes in Computer Science, vol. 9032. Springer, pp. 383–405.CrossRefGoogle Scholar
Giffin, D. B., Levy, A., Stefan, D., Terei, D., Mazières, D., Mitchell, J. & Russo, A. (2012) Hails: Protecting data privacy in untrusted web applications. In Proceedings of 10th Symposium on Operating Systems Design and Implementation, OSDI'12. USENIX Association, pp. 47–60.Google Scholar
Godefroid, P., Klarlund, N., & Sen, K. (2005) DART: Directed automated random testing. In Proceedings of 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'05. ACM, pp. 213–223.CrossRefGoogle Scholar
Goguen, J. A. & Meseguer, J. (1984) Unwinding and inference control. In Proceedings of IEEE 1984 Symposium on Security and Privacy. IEEE CS, pp. 75–87.CrossRefGoogle Scholar
Groce, A., Holzmann, G. J. & Joshi, R. (2007) Randomized differential testing as a prelude to formal verification. In Proceedings of The 29th International Conference on Software Engineering, ICSE'07. IEEE CS, pp. 621–631.CrossRefGoogle Scholar
Guernic, G. L. (2007) Automaton-based confidentiality monitoring of concurrent programs. In Proceedings of 20th Computer Security Foundations Symposium, CSF'07. IEEE CS, pp. 218–232.CrossRefGoogle Scholar
Guernic, G. L., Banerjee, A., Jensen, T. P. & Schmidt, D. A. (2006) Automata-based confidentiality monitoring. In Proceedings of 11th Asian Computing Science Conference, ASIAN 2006. Springer, pp. 75–89.Google Scholar
Hedin, D. & Sabelfeld, A. (2012) Information-flow security for a core of JavaScript. In Proceedings of 25th IEEE Computer Security Foundations Symposium (CSF), CSF'12. IEEE CS, pp. 3–18.CrossRefGoogle Scholar
Hriţcu, C., Greenberg, M., Karel, B., Pierce, B. C. & Morrisett, G. (2013a) All your IFCException are belong to us. In Proceedings of 34th IEEE Symposium on Security and Privacy, SP'13, IEEE CS, pp. 3–17.CrossRefGoogle Scholar
Hriţcu, C., Hughes, J., Pierce, B. C., Spector-Zabusky, A., Vytiniotis, D., Azevedo, de Amorim, A. & Lampropoulos, L. (2013b) Testing noninterference, quickly. In Proceedings of 18th ACM SIGPLAN International Conference on Functional Programming, ICFP'13. ACM, pp. 455–468.CrossRefGoogle Scholar
Hughes, J. (2007) QuickCheck testing for fun and profit. In Proceedings of 9th International Symposium on Practical Aspects of Declarative Languages, PADL'07, Lecture Notes in Computer Science, vol. 4354. Springer, pp. 1–32.Google Scholar
Kinder, J. (2015) Hypertesting: The case for automated testing of hyperproperties. In Proceedings of 3rd Workshop on Hot Issues in Security Principles and Trust, HotSpot.Google Scholar
Klein, C. (August 2009) Experience with randomized testing in programming language metatheory. Master's Thesis, Northwestern. Available at: http://plt.eecs.northwestern.edu/klein-masters.pdf. Accessed Feb 26, 2016.CrossRefGoogle Scholar
Klein, C., Clements, J., Dimoulas, C., Eastlund, C., Felleisen, M., Flatt, M., McCarthy, J. A., Rafkind, J., Tobin-Hochstadt, S. & Findler, R. B. (2012) Run your research: On the effectiveness of lightweight mechanization. In Proceedings of 39th ACM SIGPLAN-SIGACT Principles of Programming Languages, POPL'12, ACM, pp. 285–296.CrossRefGoogle Scholar
Klein, C. & Findler, R. B. (2009) Randomized testing in PLT Redex. In Proceedings of Workshop on Scheme and Functional Programming, SFP, ACM, pp. 26–36.Google Scholar
Klein, C., Flatt, M. & Findler, R. (2013) The Racket virtual machine and randomized testing. In Higher-Order and Symbolic Computation, Springer, pp. 1–45. http://dx.doi.org/10.1007/s10990-013-9091-1 Google Scholar
Koopman, P. W. M., Achten, P. & Plasmeijer, R. (2014) Model-based shrinking for state-based testing. In Proceedings of 14th International Symposium on Trends in Functional Programming, TFP 2013, Lecture Notes in Computer Science, vol. 8322, Springer, pp. 107–124.CrossRefGoogle Scholar
Lampropoulos, L., Pierce, B. C., Hriţcu, C., Hughes, J., Paraskevopoulou, Z. & Xia, L. (July 2015) Making our own Luck: A language for random generators. Draft. https://www.cis.upenn.edu/~llamp/pdf/Luck.pdf Google Scholar
Leroy, X., Appel, A. W., Blazy, S. & Stewart, G. (June 2012) The CompCert memory model, version 2. Research report RR-7987, INRIA.Google Scholar
Leroy, X. & Blazy, S. (2008) Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reason. 41 (1), 1–31.CrossRefGoogle Scholar
Lindblad, F. (2007) Property directed generation of first-order test data. In Proceedings of 8th Symposium on Trends in Functional Programming, TFP'07, Trends in Functional Programming, vol. 8. Intellect, pp. 105–123.Google Scholar
Majumdar, R. & Sen, K. (2007) Hybrid concolic testing. In Proceedings of 29th International Conference on Software Engineering, ICSE'07. IEEE CS, pp. 416–426.CrossRefGoogle Scholar
Milushev, D., Beck, W. & Clarke, D. (2012) Noninterference via symbolic execution. In Proceedings of Joint 14th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems and 32nd IFIP WG 6.1 International Conference, FMOODS 2012 and FORTE 2012, Lecture Notes in Computer Science, vol. 7273. Springer, pp. 152–168.CrossRefGoogle Scholar
Mohr, R. & Henderson, T. C. (1986) Arc and path consistency revisited. Artif. Intell. 28 (2), 225–233.CrossRefGoogle Scholar
Ochoa, M., Cuéllar, J., Pretschner, A. & Hallgren, P. (2015) Idea: Unwinding based model-checking and testing for non-interference on EFSMs. In Proceedings of 7th International Symposium on Engineering Secure Software and Systems, ESSoS'15, Lecture Notes in Computer Science, vol. 8978. Springer, pp. 34–42.CrossRefGoogle Scholar
Pacheco, C. & Ernst, M. D. (2007) Randoop: Feedback-directed random testing for Java. In Proceedings of 22nd ACM SIGPLAN Conference on Object-Oriented Programming Systems And Applications, OOPSLA'07. ACM, pp. 815–816.CrossRefGoogle Scholar
Paraskevopoulou, Z., Hriţcu, C., Dénès, M., Lampropoulos, L. & Pierce, B. C. (2015) Foundational property-based testing. In Proceedings of 6th International Conference on Interactive Theorem Proving, Urban, C. & Zhang, X. (eds), ITP'15, Lecture Notes in Computer Science, vol. 9236. Springer, pp. 325–343.CrossRefGoogle Scholar
Regehr, J., Chen, Y., Cuoq, P., Eide, E., Ellison, C. & Yang, X. (2012) Test-case reduction for C compiler bugs. In Proceedings of 33rd ACM SIGPLAN conference on Programming Language Design and Implementation, PLDI'12. ACM, pp. 335–346.CrossRefGoogle Scholar
Runciman, C., Naylor, M. & Lindblad, F. (2008) SmallCheck and Lazy SmallCheck: Automatic exhaustive testing for small values. In Proceedings of 1st ACM SIGPLAN Symposium on Haskell. ACM, pp. 37–48.CrossRefGoogle Scholar
Russo, A. & Sabelfeld, A. (2010) Dynamic versus static flow-sensitive security analysis. In Proceedings of 23rd Computer Security Foundations Symposium, CSF'10. IEEE CS, pp. 186–199.Google Scholar
Sabelfeld, A. & Myers, A. (January 2003) Language-based information-flow security. IEEE J. Sel. Areas Commu. 21 (1), 5–19.CrossRefGoogle Scholar
Sabelfeld, A. & Russo, A. (2010) From dynamic to static and back: Riding the roller coaster of information-flow control research. In Proceedings of 7th International Andrei Ershov Memorial Conference, PSI 2009, Lecture Notes in Computer Science, vol. 5947. Springer, pp. 352–365.CrossRefGoogle Scholar
Sabelfeld, A. & Sands, D. (2005) Dimensions and principles of declassification. In Proceedings of 18th IEEE Workshop on Computer Security Foundations, CSF'05. IEEE CS, pp. 255–269.CrossRefGoogle Scholar
Sen, K., Marinov, D. & Agha, G. (2005) CUTE: A concolic unit testing engine for C. In Proceedings of 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC/FSE-13. ACM, pp. 263–272.CrossRefGoogle Scholar
Stefan, D., Russo, A., Mitchell, J. C. & Mazières, D. (2011) Flexible dynamic information flow control in Haskell. In Proceedings of 4th Symposium on Haskell. ACM, pp. 95–106.CrossRefGoogle Scholar
Stefan, D., Russo, A., Mitchell, J. C. & Mazières, D. (July 2012) Flexible dynamic information flow control in the presence of exceptions. ArXiv e-print 1207.1457.Google Scholar
Terauchi, T. & Aiken, A. (2005) Secure information flow as a safety problem. In Proceedings of 12th International Symposium on Static Analysis, SAS 2005, Lecture Notes in Computer Science, vol. 3672. Springer, pp. 352–367.CrossRefGoogle Scholar
Torlak, E. & Bodík, R. (2014) A lightweight symbolic virtual machine for solver-aided host languages. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014. ACM, 2014, pp. 530–541.CrossRefGoogle Scholar
Williams, N., Marre, B. & Mouy, P. (2004) On-the-fly generation of K-path tests for C functions. In Proceedings of 19th IEEE International Conference on Automated Software Engineering, ASE. IEEE CS, pp. 290–293.CrossRefGoogle Scholar
Yang, X., Chen, Y., Eide, E. & Regehr, J. (2011) Finding and understanding bugs in C compilers. In Proceedings of 32nd SIGPLAN Conference on Programming Language Design and Implementation, PLDI'11, ACM, pp. 283–294.CrossRefGoogle Scholar
Zdancewic, S. A. (2002) Programming Languages for Information Security. PhD Thesis, Cornell University.Google Scholar
Zeller, A. & Hildebrandt, R. (2002) Simplifying and isolating failure-inducing input. IEEE Trans. Softw. Eng. 28 (2), 183–200.CrossRefGoogle Scholar
Zheng, L. & Myers, A. C. (2007) Dynamic security labels and static information flow control. Int. J. Inform. Secur. 6 (2–3), 67–84.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.