Marcelo Sousa
ABSTRACT
Unlike safety properties which require the absence of a “bad” program trace, k-safety properties stipulate the absence of a “bad” interaction between k traces. Examples of k-safety properties include transitivity, associativity, anti-symmetry, and monotonicity. This paper presents a sound and relatively complete calculus, called Cartesian Hoare Logic (CHL), for verifying k-safety properties. We also present an automated verification algorithm based on CHL and implement it in a tool called DESCARTES. We use DESCARTES to analyze user-defined relational operators in Java and demonstrate that DESCARTES is effective at verifying (or finding violations of) multiple k-safety properties.
- G. Barthe, P. R. D’Argenio, and T. Rezk. Secure information flow by self-composition. In Computer Security Foundations Workshop, 2004. Proceedings. 17th IEEE, pages 100–114. IEEE, 2004. Google Scholar
Digital Library
- G. Barthe, B. Grégoire, and S. Zanella Béguelin. Formal certification of code-based cryptographic proofs. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 90–101. ACM, 2009. Google ScholarDigital Library
- G. Barthe, J. M. Crespo, and C. Kunz. Relational verification using product programs. In FM 2011: Formal Methods, pages 200–214. Springer, 2011. Google ScholarDigital Library
- G. Barthe, B. Köpf, F. Olmedo, and S. Zanella Béguelin. Probabilistic relational reasoning for differential privacy. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 97–110. ACM, 2012. Google ScholarDigital Library
- G. Barthe, J. M. Crespo, and C. Kunz. Beyond 2-safety: Asymmetric product programs for relational program verification. In Logical Foundations of Computer Science, pages 29–43. Springer, 2013.Google Scholar
- N. Benton. Simple relational correctness proofs for static analyses and program transformations. In ACM SIGPLAN Notices, volume 39, pages 14–25. ACM, 2004. Google ScholarDigital Library
- A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu. Bounded model checking. Advances in computers, 58:117– 148, 2003.Google ScholarCross Ref
- C. Cadar, D. Dunbar, D. R. Engler, et al. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, volume 8, pages 209–224, 2008. Google ScholarDigital Library
- E. Clarke, D. Kroening, and F. Lerda. A tool for checking ansi-c programs. In Tools and Algorithms for the Construction and Analysis of Systems, pages 168–176. Springer, 2004.Google Scholar
- M. R. Clarkson and F. B. Schneider. Hyperproperties. In Computer Security Foundations Symposium, 2008. CSF’08. IEEE 21st, pages 51–65. IEEE, 2008. Google ScholarDigital Library
- P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 84–96. ACM, 1978. Google ScholarDigital Library
- L. De Moura and N. Bjørner. Z3: An efficient smt solver. In Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008. Google ScholarDigital Library
- J. Dean and S. Ghemawat. Mapreduce: simplified data processing on large clusters. Communications of the ACM, 51(1): 107–113, 2008. Google ScholarDigital Library
- C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for esc/java. In FME 2001: Formal Methods for Increasing Software Productivity, pages 500–517. Springer, 2001. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. Dart: directed automated random testing. In ACM Sigplan Notices, volume 40, pages 213–223. ACM, 2005. Google ScholarDigital Library
- J. A. Goguen and J. Meseguer. Security policies and security models. IEEE, 1982.Google ScholarCross Ref
- A. Miné. The octagon abstract domain. Higher-Order and Symbolic Computation, 19(1):31–100, 2006. Google ScholarDigital Library
- A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In Tools and Algorithms for the Construction and Analysis of Systems, pages 151–166. Springer, 1998. Google ScholarDigital Library
- A. Sabelfeld and A. C. Myers. Language-based informationflow security. Selected Areas in Communications, IEEE Journal on, 21(1):5–19, 2003. Google ScholarDigital Library
- R. Sharma, S. Gupta, B. Hariharan, A. Aiken, P. Liang, and A. V. Nori. A data driven approach for algebraic loop invariants. In Programming Languages and Systems, pages 574–592. Springer, 2013. Google ScholarDigital Library
- M. Sousa, I. Dillig, D. Vytiniotis, T. Dillig, and C. Gkantsidis. Consolidation of queries with user-defined functions. PLDI, 49(6):554–564, 2014. Google ScholarDigital Library
- H. Tanno, X. Zhang, T. Hoshino, and K. Sen. Tesma and catg: Automated test generation tools for models of enterprise applications. In Proceedings of the 37th International Conference on Software Engineering - Volume 2, pages 717–720. IEEE Press, 2015. Google ScholarDigital Library
- T. Terauchi and A. Aiken. Secure information flow as a safety problem. In Static Analysis Symposium (SAS). Springer, 2005. Google ScholarDigital Library
- T. White. Hadoop: The definitive guide. " O’Reilly Media, Inc.", 2012. Google ScholarDigital Library
- H. Yang. Relational separation logic. Theoretical Computer Science, 375(1):308–334, 2007. Google ScholarDigital Library
- A. Zaks and A. Pnueli. Covac: Compiler validation by program analysis of the cross-product. In FM 2008: Formal Methods, pages 35–51. Springer, 2008. Google ScholarDigital Library
Index Terms
- Cartesian hoare logic for verifying k-safety properties
Recommendations
Cartesian hoare logic for verifying k-safety properties
PLDI '16Unlike safety properties which require the absence of a “bad” program trace, k-safety properties stipulate the absence of a “bad” interaction between k traces. Examples of k-safety properties include transitivity, associativity, anti-symmetry, and ...
Verifying relational properties of functional programs by first-order refinement
We give an automated verification method for relational properties.The target is a higher-order functional language.We can use general refinement types as specifications under a certain restriction.We reduce type checking for general refinement types to ...
Verifying Relational Properties of Functional Programs by First-Order Refinement
PEPM '15: Proceedings of the 2015 Workshop on Partial Evaluation and Program ManipulationMuch progress has been made recently on fully automated verification of higher-order functional programs, based on refinement types and higher-order model checking. Most of those verification techniques are, however, based on first-order refinement ...
Comments