Niklas Grimm
Cătălin Hriţcu
ABSTRACT
Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than developing separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and game-based cryptographic security. By relying on SMT-based automation, unary weakest preconditions, user-defined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer.
- Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub. 2017. A Relational Logic for Higher-Order Programs. CoRR abs/1703.05042 (2017). http://arxiv.org/abs/1703.05042. Google Scholar
Digital Library
- Alejandro Aguirre, Catalin Hritcu, Chantal Keller, and Nikhil Swamy. 2016. From F* to SMT (extended abstract). Talk at 1st International Workshop on Hammers for Type Theories (HaTT).Google Scholar
- Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. 2017. Dijkstra Monads for Free. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, 515-529. Google ScholarDigital Library
- Amal Ahmed, Derek Dreyer, and Andreas Rossberg. 2009. State-dependent representation independence, See (Shao and Pierce 2009), 340-353. Google ScholarDigital Library
- Torben Amtoft and Anindya Banerjee. 2004. Information Flow Analysis in Logical Form. In Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings (Lecture Notes in Computer Science), Roberto Giacobazzi (Ed.), Vol. 3148. Springer, 100-115.Google Scholar
- Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew W. Appel, Lennart Beringer, John Hatcliff, Xinming Ou, and Andrew Cousino. 2012. A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow. In Principles of Security and Trust - First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012, Proceedings (Lecture Notes in Computer Science), Pierpaolo Degano and Joshua D. Guttman (Eds.), Vol. 7215. Springer, 369-389. Google ScholarDigital Library
- Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei. 2017. Decomposition Instead of Self-Composition for k-Safety. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), to appear.. http://www.f.waseda.jp/terauchi/papers/pldi17-blazer.pdf Google ScholarDigital Library
- Kazuyuki Asada, Ryosuke Sato, and Naoki Kobayashi. 2016. Verifying relational properties of functional programs by first-order refinement. Science of Computer Programming (March 2016). Google ScholarDigital Library
- Robert Atkey. 2009. Parameterised notions of computation. Journal of Functional Programming 19 (2009), 335-376. Issue 3-4. Google ScholarDigital Library
- Anindya Banerjee, David A. Naumann, and Mohammad Nikouei. 2016. Relational Logic with Framing and Hypotheses. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13-15, 2016, Chennai, India (LIPIcs), Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen (Eds.), Vol. 65. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 11:1-11:16.Google Scholar
- Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2016. Product programs and relational program logics. J. Log. Algebr. Meth. Program. 85, 5 (2016), 847-859.Google ScholarCross Ref
- Gilles Barthe, Pedro R. D'Argenio, and Tamara Rezk. 2011. Secure information flow by self-composition. Mathematical Structures in Computer Science 21, 6 (2011), 1207-1252. Google ScholarDigital Library
- Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, and Pierre-Yves Strub. 2013a. EasyCrypt: A Tutorial. In Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures (Lecture Notes in Computer Science), Alessandro Aldini, Javier Lopez, and Fabio Martinelli (Eds.), Vol. 8604. Springer, 146-166.Google Scholar
- Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella-Béguelin. 2014. Probabilistic relational verification for cryptographic implementations. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 193-206. Google ScholarDigital Library
- Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. 2015. Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 55-68. Google ScholarDigital Library
- Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin. 2009. Formal certification of code-based cryptographic proofs, See (Shao and Pierce 2009), 90-101. Google ScholarDigital Library
- Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin. 2012. Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. In 11th International Conference on Mathematics of Program Construction (Lecture Notes in Computer Science), Vol. 7342. Springer, 1-6. http://hal.inria.fr/docs/00/76/58/64/PDF/main.pdf. Google ScholarDigital Library
- Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella-Béguelin. 2013b. Probabilistic Relational Reasoning for Differential Privacy. ACM Trans. Program. Lang. Syst. 35, 3 (2013), 9:1-9:49. Google ScholarDigital Library
- Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. 2016. CoSMed: A Confidentiality-Verified Social Media Platform. In Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings (Lecture Notes in Computer Science), Jasmin Christian Blanchette and Stephan Merz (Eds.), Vol. 9807. Springer, 87-106.Google Scholar
- Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. 2017. CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees. In 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017. IEEE Computer Society, 729-748.Google Scholar
- Bernhard Beckert, Vladimir Klebanov, and Mattias Ulbrich. 2015. Regression verification for Java using a secure information flow calculus. In Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015, Prague, Czech Republic, July 7, 2015, Rosemary Monahan (Ed.). ACM, 6:1-6:6. Google ScholarDigital Library
- Mihir Bellare and Phillip Rogaway. 2006. The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs. In Advances in Cryptology - EUROCRYPT 2006. 409-426. Google ScholarDigital Library
- Nick Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '04). ACM, New York, NY, USA, 14-25. Google ScholarDigital Library
- Nick Benton, Martin Hofmann, and Vivek Nigam. 2013. Proof-Relevant Logical Relations for Name Generation. In 11th International Conference on Typed Lambda Calculi and Applications (Lecture Notes in Computer Science), Vol. 7941. Springer, 48-60.Google Scholar
- Nick Benton, Martin Hofmann, and Vivek Nigam. 2014. Abstract effects and proof-relevant logical relations. In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 619-632. Google ScholarDigital Library
- Nick Benton, Andrew Kennedy, Lennart Beringer, and Martin Hofmann. 2009. Relational semantics for effect-based program transformations: higher-order store. In Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal, António Porto and Francisco Javier López-Fraguas (Eds.). ACM, 301-312. Google ScholarDigital Library
- Nick Benton, Andrew Kennedy, Martin Hofmann, and Lennart Beringer. 2006. Reading, Writing and Relations. In Programming Languages and Systems, 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8- 10, 2006, Proceedings (Lecture Notes in Computer Science), Naoki Kobayashi (Ed.), Vol. 4279. Springer, 114-130. Google ScholarDigital Library
- Nick Benton, Andrew Kennedy, Martin Hofmann, and Vivek Nigam. 2016. Counting Successes: Effects and Transformations for Nondeterministic Programs. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Lecture Notes in Computer Science), Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella (Eds.), Vol. 9600. Springer, 56-72.Google Scholar
- Lennart Beringer and Martin Hofmann. 2007. Secure information flow and program logics. In 20th IEEE Computer Security Foundations Symposium, CSF 2007, 6-8 July 2007, Venice, Italy. IEEE Computer Society, 233-248. Google ScholarDigital Library
- Bruno Blanchet, Martín Abadi, and Cédric Fournet. 2008. Automated verification of selected equivalences for security protocols. J. Log. Algebr. Program. 75, 1 (2008), 3-51.Google ScholarCross Ref
- Michael Carbin, Deokhwan Kim, Sasa Misailovic, and Martin C. Rinard. 2012. Proving acceptability properties of relaxed nondeterministic approximate programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12, Beijing, China - June 11 - 16, 2012, Jan Vitek, Haibo Lin, and Frank Tip (Eds.). ACM, 169-180. Google ScholarDigital Library
- Rohit Chadha, Vincent Cheval, Stefan Ciobâca, and Steve Kremer. 2016. Automated Verification of Equivalence Properties of Cryptographic Protocols. ACM Trans. Comput. Log. 17, 4 (2016), 23:1-23:32. http://dl.acm.org/citation.cfm?id=2926715. Google ScholarDigital Library
- Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. 2017. Relational cost analysis. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 316-329. Google ScholarDigital Library
- Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. J. Comput. Secur. 18, 6 (Sept. 2010), 1157-1210. https://www.cs.cornell.edu/fbs/publications/Hyperproperties.pdf. Google ScholarDigital Library
- Stefan Ciobâca, Dorel Lucanu, Vlad Rusu, and Grigore Rosu. 2016. A language-independent proof system for full program equivalence. Formal Asp. Comput. 28, 3 (2016), 469-497. Google ScholarCross Ref
- Ádám Darvas, Reiner Hähnle, and David Sands. 2005. A Theorem Proving Approach to Analysis of Secure Information Flow. In Security in Pervasive Computing, Second International Conference, SPC 2005, Boppard, Germany, April 6-8, 2005, Proceedings (Lecture Notes in Computer Science), Dieter Hutter and Markus Ullmann (Eds.), Vol. 3450. Springer, 193-209. Google ScholarDigital Library
- Derek Dreyer, Amal Ahmed, and Lars Birkedal. 2011. Logical Step-Indexed Logical Relations. Logical Methods in Computer Science 7, 2 (2011).Google Scholar
- Derek Dreyer, Georg Neis, and Lars Birkedal. 2012. The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program. 22, 4-5 (2012), 477-528. Google ScholarDigital Library
- Derek Dreyer, Georg Neis, Andreas Rossberg, and Lars Birkedal. 2010. A relational modal logic for higher-order stateful ADTs. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 185-198. Google ScholarDigital Library
- Stefan Fehrenbach and James Cheney. 2016. Language-integrated provenance. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016, James Cheney and Germán Vidal (Eds.). ACM, 214-227. Google ScholarDigital Library
- Andrzej Filinski. 1994. Representing Monads. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '94). ACM, New York, NY, USA, 446-457. Google ScholarDigital Library
- Benny Godlin and Ofer Strichman. 2010. Inference Rules for Proving the Equivalence of Recursive Procedures. In Time for Verification, Essays in Memory of Amir Pnueli (Lecture Notes in Computer Science), Zohar Manna and Doron A. Peled (Eds.), Vol. 6200. Springer, 167-184. Google ScholarDigital Library
- J. A. Goguen and J. Meseguer. 1982. Security Policies and Security Models. 1982 IEEE Symposium on Security and Privacy 00 (1982), 11.Google Scholar
- Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin. 2017. A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations. arXiv:1703.00055. https://arxiv.org/abs/1703.00055. Google ScholarDigital Library
- Christian Hammer and Gregor Snelting. 2009. Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int. J. Inf. Sec. 8, 6 (2009), 399-422. Google ScholarDigital Library
- Shaobo He, Shuvendu K. Lahiri, and Zvonimir Rakamaric. 2016. Verifying Relative Safety, Accuracy, and Termination for Program Approximations. In NASA Formal Methods - 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings (Lecture Notes in Computer Science), Sanjai Rayadurgam and Oksana Tkachuk (Eds.), Vol. 9690. Springer, 237-254. Google ScholarDigital Library
- Daniel Hedin and Andrei Sabelfeld. 2012. A Perspective on Information-Flow Control. In Software Safety and Security - Tools for Analysis and Verification, Tobias Nipkow, Orna Grumberg, and Benedikt Hauptmann (Eds.). NATO Science for Peace and Security Series - D: Information and Communication Security, Vol. 33. IOS Press, 319-347.Google Scholar
- Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis. 2012. The marriage of bisimulations and Kripke logical relations. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, John Field and Michael Hicks (Eds.). ACM, 59-72. Google ScholarDigital Library
- Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. 2014. A Logical Step Forward in Parametric Bisimulations. Technical Report MPI-SWS-2014-003. http://sf.snu.ac.kr/gil.hur/publications/spbs.pdf.Google Scholar
- Vasileios Koutavas and Mitchell Wand. 2006. Small bisimulations for reasoning about higher-order imperative programs. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, J. Gregory Morrisett and Simon L. Peyton Jones (Eds.). ACM, 141-152. Google ScholarDigital Library
- Sudipta Kundu, Zachary Tatlock, and Sorin Lerner. 2009. Proving optimizations correct using parameterized program equivalence. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, June 15- 21, 2009, Michael Hind and Amer Diwan (Eds.). ACM, 327-337. Google ScholarDigital Library
- Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten, and Martin Mohr. 2015. A Hybrid Approach for Proving Noninterference of Java Programs. In IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13-17 July, 2015, Cédric Fournet, Michael W. Hicks, and Luca Viganò (Eds.). IEEE Computer Society, 305- 319. Google ScholarDigital Library
- Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, and Henrique Rebêlo. 2012. SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings (Lecture Notes in Computer Science), P. Madhusudan and Sanjit A. Seshia (Eds.), Vol. 7358. Springer, 712-717. Google ScholarDigital Library
- Dorel Lucanu and Vlad Rusu. 2015. Program equivalence by circular reasoning. Formal Asp. Comput. 27, 4 (2015), 701-726. Google ScholarCross Ref
- Conor McBride. 2015. Turing-Completeness Totally Free. In Mathematics of Program Construction - 12th International Conference, MPC 2015, Königswinter, Germany, June 29 - July 1, 2015. Proceedings (Lecture Notes in Computer Science), Ralf Hinze and Janis Voigtländer (Eds.), Vol. 9129. Springer, 257-275.Google Scholar
- John C. Mitchell. 1986. Representation independence and data abstraction. In POPL '86. ACM, New York, NY, USA, 263-276. Google ScholarDigital Library
- Eugenio Moggi. 1989. Computational Lambda-Calculus and Monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989. IEEE Computer Society, 14-23. Google ScholarDigital Library
- Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. 2013. seL4: From General Purpose to a Proof of Information Flow Enforcement. In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013. IEEE Computer Society, 415-429. Google ScholarDigital Library
- Aleksandar Nanevski, Anindya Banerjee, and Deepak Garg. 2013. Dependent Type Theory for Verification of Information Flow and Access Control Policies. ACM Transactions on Programming Languages and Systems 35, 2 (2013), 6. Google ScholarDigital Library
- Aleksandar Nanevski, J. Gregory Morrisett, and Lars Birkedal. 2008. Hoare type theory, polymorphism and separation. J. Funct. Program. 18, 5-6 (2008), 865-911. http://ynot.cs.harvard.edu/papers/jfpsep07.pdf. Google ScholarDigital Library
- David A. Naumann. 2006. From Coupling Relations to Mated Invariants for Checking Information Flow. In Computer Security - ESORICS 2006, 11th European Symposium on Research in Computer Security, Hamburg, Germany, September 18-20, 2006, Proceedings (Lecture Notes in Computer Science), Dieter Gollmann, Jan Meier, and Andrei Sabelfeld (Eds.), Vol. 4189. Springer, 279-296. Google ScholarDigital Library
- Aleksey Nogin. 2002. Quotient Types: A Modular Approach. In 15th International Conference on Theorem Proving in Higher Order Logics (Lecture Notes in Computer Science), Vol. 2410. Springer, 263-280. Google ScholarDigital Library
- Adam Petcher and Greg Morrisett. 2015. The Foundational Cryptography Framework. In Principles of Security and Trust - 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings (Lecture Notes in Computer Science), Riccardo Focardi and Andrew C. Myers (Eds.), Vol. 9036. Springer, 53-72. Google ScholarDigital Library
- Simon Peyton Jones. 2010. Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. IOS Press, 47-96. https://www.microsoft.com/en-us/research/publication/tackling-awkward-squad-monadic-inputoutput-concurrency-exceptions-foreign-language-calls-haskell/.Google Scholar
- Markus N. Rabe. 2016. A temporal logic approach to Information-flow control. Ph.D. Dissertation. Saarland University. http://scidok.sulb.uni-saarland.de/volltexte/2016/6387/.Google Scholar
- Andrei Sabelfeld and Andrew C. Myers. 2003. Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21, 1 (2003), 5-19. Google ScholarDigital Library
- A. Sabelfeld and A. C. Myers. 2006. Language-based Information-flow Security. IEEE J.Sel. A. Commun. 21, 1 (Sept. 2006), 5-19. Google ScholarDigital Library
- Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. 2011. Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst. 33, 1 (2011), 5:1-5:69. Google ScholarDigital Library
- Christoph Scheben and Peter H. Schmitt. 2011. Verification of Information Flow Properties of Java Programs without Approximations. In Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2011, Turin, Italy, October 5-7, 2011, Revised Selected Papers (Lecture Notes in Computer Science), Bernhard Beckert, Ferruccio Damiani, and Dilian Gurov (Eds.), Vol. 7421. Springer, 232-249. Google ScholarDigital Library
- Zhong Shao and Benjamin C. Pierce (Eds.). 2009. Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009. ACM. http://dl.acm.org/citation.cfm?id=1480881.Google Scholar
- Marcelo Sousa and Isil Dillig. 2016. Cartesian hoare logic for verifying k-safety properties. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, Chandra Krintz and Emery Berger (Eds.). ACM, 57-69. Google ScholarDigital Library
- Eijiro Sumii. 2009. A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References. In Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings (Lecture Notes in Computer Science), Erich Grädel and Reinhard Kahle (Eds.), Vol. 5771. Springer, 455-469. Google ScholarDigital Library
- Nikhil Swamy, Nataliya Guts, Daan Leijen, and Michael Hicks. 2011. Lightweight monadic programming in ML. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011 (ICFP '11). 15-27. https://www.cs.umd.edu/~mwh/papers/swamy11monad.html. Google ScholarDigital Library
- Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 256-270. https://www.fstarlang.org/papers/mumon/. Google ScholarDigital Library
- Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. 2013. Verifying Higher-order Programs with the Dijkstra Monad. In Proceedings of the 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI '13). 387- 398. https://www.microsoft.com/en-us/research/publication/verifying-higher-order-programs-with-the-dijkstra-monad/. Google ScholarDigital Library
- Tachio Terauchi and Alexander Aiken. 2005. Secure Information Flow as a Safety Problem. In Static Analysis, 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, Proceedings (Lecture Notes in Computer Science), Chris Hankin and Igor Siveroni (Eds.), Vol. 3672. Springer, 352-367. Google ScholarDigital Library
- Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. 1996. A Sound Type System for Secure Flow Analysis. J. Comput. Secur. 4, 2-3 (Jan. 1996), 167-187. http://dl.acm.org/citation.cfm?id=353629.353648. Google ScholarDigital Library
- Hongseok Yang. 2007. Relational separation logic. Theor. Comput. Sci. 375, 1-3 (2007), 308-334. Google ScholarDigital Library
- Hirotoshi Yasuoka and Tachio Terauchi. 2014. Quantitative information flow as safety and liveness hyperproperties. Theor. Comput. Sci. 538 (2014), 167-182.Google ScholarCross Ref
- Anna Zaks and Amir Pnueli. 2008. CoVaC: Compiler Validation by Program Analysis of the Cross-Product. In FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26- 30, 2008, Proceedings (Lecture Notes in Computer Science), Jorge Cuéllar, T. S. E. Maibaum, and Kaisa Sere (Eds.), Vol. 5014. Springer, 35-51. Google ScholarDigital Library
- Danfeng Zhang and Daniel Kifer. 2017. LightDP: towards automating differential privacy proofs. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, 888-901. http://www.cse.psu.edu/~dbz5017/pub/popl17.pdf. Google ScholarDigital Library
Index Terms
- A monadic framework for relational verification: applied to information security, program equivalence, and optimizations
Recommendations
Dependent types and multi-monadic effects in F*
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesWe present a new, completely redesigned, version of F*, a language that works both as a proof assistant as well as a general-purpose, verification-oriented, effectful programming language. In support of these complementary roles, F* is a dependently ...
An Interface Theory for Program Verification
Leveraging Applications of Formal Methods, Verification and Validation: Verification PrinciplesAbstractProgram verification is the problem, for a given program and a specification , of constructing a proof of correctness for the statement “program satisfies specification ” () or a proof of violation ([inline-graphic not available: see fulltext]). ...
Constraint-Based Relational Verification
Computer Aided VerificationAbstractIn recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses () empower a wide range of verification techniques and tools, they lack the ability to express ...
Comments