Document Open Access Logo

Relational Logic with Framing and Hypotheses

Authors Anindya Banerjee, David A. Naumann, Mohammad Nikouei

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2016.11.pdf
  • Filesize: 0.54 MB
  • 16 pages

Document Identifiers

Author Details

Anindya Banerjee
David A. Naumann
Mohammad Nikouei

Cite AsGet BibTex

Anindya Banerjee, David A. Naumann, and Mohammad Nikouei. Relational Logic with Framing and Hypotheses. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSTTCS.2016.11

Abstract

Relational properties arise in many settings: relating two versions of a program that use different data representations, noninterference properties for security, etc. The main ingredient of relational verification, relating aligned pairs of intermediate steps, has been used in numerous guises, but existing relational program logics are narrow in scope. This paper introduces a logic based on novel syntax that weaves together product programs to express alignment of control flow points at which relational formulas are asserted. Correctness judgments feature hypotheses with relational specifications, discharged by a rule for the linking of procedure implementations. The logic supports reasoning about program-pairs containing both similar and dissimilar control and data structures. Reasoning about dynamically allocated objects is supported by a frame rule based on frame conditions amenable to SMT provers. We prove soundness and sketch how the logic can be used for data abstraction, loop optimizations, and secure information flow.
Keywords
  • Relational Hoare logic
  • program equivalence
  • product programs
  • frame conditions
  • region logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Amal Ahmed, Derek Dreyer, and Andreas Rossberg. State-dependent representation independence. In ACM Symposium on Principles of Programming Languages, 2009. Google Scholar
  2. T. Amtoft, S. Bandhakavi, and A. Banerjee. A logic for information flow in object-oriented programs. In ACM Symposium on Principles of Programming Languages, 2006. Google Scholar
  3. Anindya Banerjee and David A. Naumann. Ownership confinement ensures representation independence for object-oriented programs. Journal of the ACM, 52(6):894-960, 2005. Google Scholar
  4. Anindya Banerjee and David A. Naumann. Stack-based access control for secure information flow. Journal of Functional Programming, 15(2):131-177, 2005. Google Scholar
  5. Anindya Banerjee and David A. Naumann. Local reasoning for global invariants, part II: Dynamic boundaries. Journal of the ACM, 60(3):19:1-19:73, 2013. Google Scholar
  6. Anindya Banerjee and David A. Naumann. A logical analysis of framing for specifications with pure method calls. In Verified Software: Theories, Tools and Experiments, volume 8471 of LNCS, 2014. Google Scholar
  7. Anindya Banerjee, David A. Naumann, and Mohammad Nikouei. A logical analysis of framing for specifications with pure method calls. Under review for publication. Extended version of [6]. http://www.cs.stevens.edu/~naumann/pub/readRL.pdf, 2015.
  8. Anindya Banerjee, David A. Naumann, and Stan Rosenberg. Expressive declassification policies and modular static enforcement. In IEEE Symposium on Security and Privacy, 2008. Google Scholar
  9. Anindya Banerjee, David A. Naumann, and Stan Rosenberg. Regional logic for local reasoning about global invariants. In European Conference on Object-Oriented Programming, volume 5142 of LNCS, 2008. Google Scholar
  10. Anindya Banerjee, David A. Naumann, and Stan Rosenberg. Local reasoning for global invariants, part I: Region logic. Journal of the ACM, 60(3):18:1-18:56, 2013. Google Scholar
  11. Gilles Barthe, Juan Manuel Crespo, and César Kunz. Relational verification using product programs. In Formal Methods, volume 6664 of LNCS, 2011. Google Scholar
  12. Gilles Barthe, Juan Manuel Crespo, and César Kunz. Beyond 2-safety: Asymmetric product programs for relational program verification. In Logical Foundations of Computer Science, International Symposium, volume 7734 of LNCS, 2013. Google Scholar
  13. Gilles Barthe, Juan Manuel Crespo, and César Kunz. Product programs and relational program logics. J. Logical and Algebraic Methods in Programming, 2016. To appear. Google Scholar
  14. Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. Probabilistic relational reasoning for differential privacy. ACM Trans. Program. Lang. Syst., 35(3):9, 2013. Google Scholar
  15. Nick Benton. Simple relational correctness proofs for static analyses and program transformations. In ACM Symposium on Principles of Programming Languages, 2004. Google Scholar
  16. Nick Benton, Martin Hofmann, and Vivek Nigam. Abstract effects and proof-relevant logical relations. In ACM Symposium on Principles of Programming Languages, 2014. Google Scholar
  17. Nick Benton, Andrew Kennedy, Lennart Beringer, and Martin Hofmann. Relational semantics for effect-based program transformations with dynamic allocation. In International Symposium on Principles and Practice of Declarative Programming, 2007. Google Scholar
  18. Lennart Beringer. Relational decomposition. In Interactive Theorem Proving (ITP), volume 6898 of LNCS, 2011. Google Scholar
  19. Lars Birkedal and Hongseok Yang. Relational parametricity and separation logic. Logical Methods in Computer Science, 4(2), 2008. URL: http://dx.doi.org/10.2168/LMCS-4(2:6)2008.
  20. Derek Dreyer, Georg Neis, Andreas Rossberg, and Lars Birkedal. A relational modal logic for higher-order stateful ADTs. In ACM Symposium on Principles of Programming Languages, 2010. Google Scholar
  21. Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, and Mattias Ulbrich. Automating regression verification. In International Conference on Automated Software Engineering, 2014. Google Scholar
  22. Robert W. Floyd. Assigning meanings to programs. In Proceedings of Symposia in Applied Mathematics 19, pages 19-32. American Mathematical Society, 1967. Google Scholar
  23. Benny Godlin and Ofer Strichman. Inference rules for proving the equivalence of recursive procedures. Acta Inf., 45(6):403-439, 2008. Google Scholar
  24. Benny Godlin and Ofer Strichman. Regression verification: proving the equivalence of similar programs. Softw. Test., Verif. Reliab., 23(3):241-258, 2013. Google Scholar
  25. Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, and Henrique Rebêlo. Towards modularly comparing programs using automated theorem provers. In International Conference on Automated Deduction, 2013. Google Scholar
  26. C. A. R. Hoare. Proofs of correctness of data representations. Acta Informatica, 1:271-281, 1972. Google Scholar
  27. Ioannis T. Kassios. The dynamic frames theory. Formal Aspects of Computing, 23(3):267-288, 2011. URL: http://dx.doi.org/10.1007/s00165-010-0152-5.
  28. Máté Kovács, Helmut Seidl, and Bernd Finkbeiner. Relational abstract interpretation for the verification of 2-hypersafety properties. In ACM Conference on Computer and Communications Security, 2013. Google Scholar
  29. Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, and Chris Hawblitzel. Differential assertion checking. In Joint Meeting of the European Software Engineering Conference and the ACM Symposium on the Foundations of Software Engineering, 2013. Google Scholar
  30. Gary T. Leavens and Peter Müller. Information hiding and visibility in interface specifications. In International Conference on Software Engineering, 2007. Google Scholar
  31. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, LNCS, 2010. Google Scholar
  32. Christian Mueller, Máté Kovács, and Helmut Seidl. An analysis of universal information flow based on self-composition. In IEEE Computer Security Foundations Symposium, 2015. Google Scholar
  33. Kedar S. Namjoshi and Nimit Singhania. Loopy: Programmable and formally verified loop transformations. In Static Analysis Symposium, volume 9837 of LNCS, 2016. Google Scholar
  34. Aleksandar Nanevski, Anindya Banerjee, and Deepak Garg. Dependent type theory for verification of information flow and access control policies. ACM Trans. Program. Lang. Syst., 35(2):6, 2013. URL: http://dx.doi.org/10.1145/2491522.2491523.
  35. David A. Naumann. From coupling relations to mated invariants for secure information flow. In European Symposium on Research in Computer Security, volume 4189 of LNCS, 2006. Google Scholar
  36. David A. Naumann. Observational purity and encapsulation. Theoretical Computer Science, 376(3):205-224, 2007. Google Scholar
  37. Peter W. O'Hearn, Hongseok Yang, and John C. Reynolds. Separation and information hiding. ACM Transactions on Programming Languages and Systems, 31(3):1-50, 2009. Google Scholar
  38. John C. Reynolds. The Craft of Programming. Prentice-Hall, 1981. Google Scholar
  39. John C. Reynolds. Types, abstraction, and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 1983, pages 513-523. North-Holland, 1984. Google Scholar
  40. Stan Rosenberg, Anindya Banerjee, and David A. Naumann. Decision procedures for region logic. In Int'l Conf. on Verification, Model Checking, and Abstract Interpretation, 2012. Google Scholar
  41. Marcelo Sousa and Isil Dillig. Cartesian Hoare logic for verifying k-safety properties. In ACM Conf. on Program. Lang. Design and Implementation, 2016. Google Scholar
  42. Tachio Terauchi and Alex Aiken. Secure information flow as a safety problem. In International Static Analysis Symposium, volume 3672 of LNCS, 2005. Google Scholar
  43. Jacob Thamsborg, Lars Birkedal, and Hongseok Yang. Two for the price of one: Lifting separation logic assertions. Logical Methods in Computer Science, 8(3), 2012. Google Scholar
  44. Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):167-187, 1996. Google Scholar
  45. Hongseok Yang. Relational separation logic. Theoretical Computer Science, 375(1-3):308-334, 2007. Google Scholar
  46. Anna Zaks and Amir Pnueli. CoVaC: Compiler validation by program analysis of the cross-product. In Formal Methods, volume 5014 of LNCS, 2008. Google Scholar
  47. Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg, Clark W. Barrett, Yi Fang, and Ying Hu. Translation and run-time validation of loop transformations. Formal Methods in System Design, 27(3):335-360, 2005. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact