More Web Proxy on the site http://driver.im/

research-article

Open access

Securing Verified IO Programs Against Unverified Code in F*

Authors:

Cezar-Constantin Andrici,

Ștefan Ciobâcă,

Cătălin Hriţcu,

Guido Martínez,

Exequiel Rivas,

Théo WinterhalterAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 8, Issue POPL

Article No.: 74, Pages 2226 - 2259

https://doi.org/10.1145/3632916

Published: 05 January 2024 Publication History

Abstract

We introduce SCIO*, a formally secure compilation framework for statically verified programs performing input-output (IO). The source language is an F* subset in which a verified program interacts with its IO-performing context via a higher-order interface that includes refinement types as well as pre- and post-conditions about past IO events. The target language is a smaller F* subset in which the compiled program is linked with an adversarial context that has an interface without refinement types, pre-conditions, or concrete post-conditions. To bridge this interface gap and make compilation and linking secure we propose a formally verified combination of higher-order contracts and reference monitoring for recording and controlling IO operations. Compilation uses contracts to convert the logical assumptions the program makes about the context into dynamic checks on each context-program boundary crossing. These boundary checks can depend on information about past IO events stored in the state of the monitor. But these checks cannot stop the adversarial target context before it performs dangerous IO operations. Therefore linking in SCIO* additionally forces the context to perform all IO actions via a secure IO library, which uses reference monitoring to dynamically enforce an access control policy before each IO operation. We prove in F* that SCIO* soundly enforces a global trace property for the compiled verified program linked with the untrusted context. Moreover, we prove in F* that SCIO* satisfies by construction Robust Relational Hyperproperty Preservation, a very strong secure compilation criterion. Finally, we illustrate SCIO* at work on a simple web server example.

References

[1]

2023. Dafny Reference Manual. https://dafny.org/latest/DafnyRef/DafnyRef

[2]

Johannes Åman Pohjola, Henrik Rostedt, and Magnus O. Myreen. 2019. Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. In 10th International Conference on Interactive Theorem Proving (ITP), John Harrison, John O’Leary, and Andrew Tolmach (Eds.) (LIPIcs, Vol. 141). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 32:1–32:19. https://doi.org/10.4230/LIPIcs.ITP.2019.32

[3]

Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Cătălin Hriţcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, and Andrew Tolmach. 2018. When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. In 25th ACM Conference on Computer and Communications Security (CCS). ACM, 1351–1368. arxiv:1802.00588

[4]

Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and Jérémy Thibault. 2019. Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. In 32nd IEEE Computer Security Foundations Symposium (CSF). IEEE, 256–271. https://doi.org/10.1109/CSF.2019.00025

[5]

Pieter Agten, Bart Jacobs, and Frank Piessens. 2015. Sound Modular Verification of C Code Executing in an Unverified Context. In 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Sriram K. Rajamani and David Walker (Eds.). ACM, 581–594. https://doi.org/10.1145/2676726.2676972

[6]

Pieter Agten, Raoul Strackx, Bart Jacobs, and Frank Piessens. 2012. Secure Compilation to Modern Processors. In 25th IEEE Computer Security Foundations Symposium (CSF), Stephen Chong (Ed.). IEEE Computer Society, 171–185. https://doi.org/10.1109/CSF.2012.12

[7]

Danel Ahman, Cătălin Hriţcu, 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. https://doi.org/10.1145/3009837.3009878

[8]

Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. In 3rd Workshop on Coq for Programming Languages (CoqPL). https://popl17.sigplan.org/details/main/9/CertiCoq-A-verified-compiler-for-Coq

[9]

James Anderson. 1973. Computer Security Technology Planning Study. ESD-TR-73-51, US Air Force Electronic Systems Division (1973). Section 4.1.1. http://csrc.nist.gov/publications/history/ande72.pdf

[10]

Cezar-Constantin Andrici, Stefan Ciobâcă, Cătălin Hritcu, Guido Martínez, Exequiel Rivas, Éric Tanter, and Théo Winterhalter. 2023. Artifact for the POPL 2024 paper ‘Securing Verified IO Programs Against Unverified Code in F*’. Zenodo. https://doi.org/10.5281/zenodo.10125015

[11]

Cezar-Constantin Andrici, Stefan Ciobâcă, Cătălin Hritcu, Guido Martínez, Exequiel Rivas, Éric Tanter, and Théo Winterhalter. 2023. Artifact for the POPL 2024 paper ‘Securing Verified IO Programs Against Unverified Code in F*’. GitHub. https://github.com/andricicezar/fstar-io/tree/popl24/sciostar

[12]

Andrew W. Appel. 2016. Modular Verification for Computer Security. In 29th IEEE Computer Security Foundations Symposium (CSF). IEEE Computer Society, 1–8. https://doi.org/10.1109/CSF.2016.8

[13]

Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, and Ravi Ramamurthy. 2023. FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores. In 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic (Eds.). ACM, 30–46. https://doi.org/10.1145/3573105.3575687

[14]

Pavel Avgustinov, Julian Tibble, and Oege de Moor. 2007. Making trace monitors feasible. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Richard P. Gabriel, David F. Bacon, Cristina Videira Lopes, and Guy L. Steele Jr. (Eds.). ACM, 589–608. https://doi.org/10.1145/1297027.1297070

[15]

Johannes Bader, Jonathan Aldrich, and Éric Tanter. 2018. Gradual Program Verification. In 19th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Isil Dillig and Jens Palsberg (Eds.) (Lecture Notes in Computer Science, Vol. 10747). Springer, 25–46. https://doi.org/10.1007/978-3-319-73721-8_2

[16]

Andrej Bauer and Matija Pretnar. 2015. Programming with algebraic effects and handlers. J. Log. Algebraic Methods Program., 84, 1 (2015), 108–123. https://doi.org/10.1016/j.jlamp.2014.02.001

[17]

Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, and Tim Würtele. 2021. DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code. In IEEE European Symposium on Security and Privacy (EuroS&P). IEEE, 523–542. https://doi.org/10.1109/EuroSP51992.2021.00042

[18]

Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, and Tim Würtele. 2021. An In-Depth Symbolic Security Analysis of the ACME Standard. In ACM SIGSAC Conference on Computer and Communications Security (CCS), Yongdae Kim, Jong Kim, Giovanni Vigna, and Elaine Shi (Eds.). ACM, 2601–2617. https://doi.org/10.1145/3460120.3484588

[19]

Eric Bodden, Laurie J. Hendren, and Ondrej Lhoták. 2007. A Staged Static Program Analysis to Improve the Performance of Runtime Monitoring. In 21st European Conference on Object-oriented Programming (ECOOP), Erik Ernst (Ed.) (Lecture Notes in Computer Science, Vol. 4609). Springer, 525–549. https://doi.org/10.1007/978-3-540-73589-2_25

[20]

Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath T. V. Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. In 26th USENIX Security Symposium, Engin Kirda and Thomas Ristenpart (Eds.). USENIX Association, 917–934. https://www.usenix.org/conference/usenixsecurity17/technical-sessions/presentation/bond

[21]

Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann. 2020. Effects as capabilities: effect handlers and lightweight effect polymorphism. Proc. ACM Program. Lang., 4, OOPSLA (2020), 126:1–126:30. https://doi.org/10.1145/3428194

[22]

Feng Chen, Marcelo D’Amorim, and Grigore Roşu. 2004. A Formal Monitoring-Based Framework for Software Development and Analysis. In Formal Methods and Software Engineering. Springer Berlin Heidelberg, 357–372. https://doi.org/10.1007/978-3-540-30482-1_31

[23]

Feng Chen and Grigore Roşu. 2005. Java-MOP: A Monitoring Oriented Programming Environment for Java. In Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 546–550. https://doi.org/10.1007/978-3-540-31980-1_36

[24]

Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. J. Comput. Secur., 18, 6 (2010), Sept., 1157–1210. issn:0926-227X https://www.cs.cornell.edu/fbs/publications/Hyperproperties.pdf

[25]

David R. Cok and K. Rustan M. Leino. 2022. Specifying the Boundary Between Unverified and Verified Code. In The Logic of Software. A Tasting Menu of Formal Methods - Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday, Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, and Einar Broch Johnsen (Eds.) (Lecture Notes in Computer Science, Vol. 13360). Springer, 105–128. https://doi.org/10.1007/978-3-031-08166-8_6

[26]

Pierre-Évariste Dagand, Nicolas Tabareau, and Éric Tanter. 2018. Foundations of dependent interoperability. J. Funct. Program., 28 (2018), e9. https://doi.org/10.1017/S0956796818000011

[27]

Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin, Karthikeyan Bhargavan, Jianyang Pan, and Jean Karim Zinzindohoue. 2017. Implementing and Proving the TLS 1.3 Record Layer. In 2017 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society, 463–482. https://doi.org/10.1109/SP.2017.58

[28]

Dominique Devriese, Marco Patrignani, Frank Piessens, and Steven Keuchel. 2017. Modular, Fully-abstract Compilation by Approximate Back-translation. Log. Methods Comput. Sci., 13, 4 (2017), https://doi.org/10.23638/LMCS-13(4:2)2017

[29]

Tim Disney, Cormac Flanagan, and Jay McCarthy. 2011. Temporal higher-order contracts. In 16th ACM SIGPLAN international conference on Functional Programming (ICFP), Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy (Eds.). ACM, 176–188. https://doi.org/10.1145/2034773.2034800

[30]

Rémi Douence, Pascal Fradet, and Mario Südholt. 2005. Trace-Based Aspects. In Aspect-Oriented Software Development, Robert E. Filman, Tzilla Elrad, Siobhán Clarke, and Mehmet Akşit (Eds.). Addison-Wesley, Boston. 201–217. https://inria.hal.science/inria-00000947/fr/

[31]

Akram El-Korashy, Stelios Tsampas, Marco Patrignani, Dominique Devriese, Deepak Garg, and Frank Piessens. 2021. CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle. In 34th IEEE Computer Security Foundations Symposium (CSF). IEEE, 1–16. https://doi.org/10.1109/CSF51468.2021.00036

[32]

Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, and Son Ho. 2018. Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications. In 10th International Conference on Verified Software. Theories, Tools, and Experiments (VSTTE), Ruzica Piskac and Philipp Rümmer (Eds.) (Lecture Notes in Computer Science, Vol. 11294). Springer, 88–111. https://doi.org/10.1007/978-3-030-03592-1_6

[33]

Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for higher-order functions. In 7th ACM SIGPLAN International Conference on Functional Programming (ICFP), Mitchell Wand and Simon L. Peyton Jones (Eds.). ACM, 48–59. https://doi.org/10.1145/581478.581484

[34]

Matthew Flatt and PLT. [n. d.]. The Racket Reference. https://docs.racket-lang.org/reference/

[35]

Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy. 2019. A Verified, Efficient Embedding of a Verifiable Assembly Language. PACMPL, 3, POPL (2019), https://github.com/project-everest/project-everest.github.io/raw/master/assets/vale-popl.pdf

[36]

Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux, and Tahina Ramananandro. 2021. Steel: proof-oriented programming in a dependently typed concurrent separation logic. Proc. ACM Program. Lang., 5, ICFP (2021), 1–30. https://doi.org/10.1145/3473590

[37]

Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin. 2018. A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations. In The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. arxiv:1703.00055

[38]

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Kimberly Keeton and Timothy Roscoe (Eds.). USENIX Association, 653–669. https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu

[39]

Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, and Derek Dreyer. 2023. Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. Proc. ACM Program. Lang., 7, OOPSLA2 (2023), Article 247, oct, 29 pages. https://doi.org/10.1145/3622823

[40]

Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, and Michael Norrish. 2017. Verified Characteristic Formulae for CakeML. In 26th European Symposium on Programming (ESOP), Hongseok Yang (Ed.) (Lecture Notes in Computer Science, Vol. 10201). Springer, 584–610. https://doi.org/10.1007/978-3-662-54434-1_22

[41]

Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno. 2020. Storage Systems are Distributed Systems (So Verify Them That Way!). In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI). https://www.andrew.cmu.edu/user/bparno/papers/veribetrkv.pdf

[42]

Son Ho, Jonathan Protzenko, Abhishek Bichhawat, and Karthikeyan Bhargavan. 2022. Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations. In 43rd IEEE Symposium on Security and Privacy (SP). IEEE, 107–124. https://doi.org/10.1109/SP46214.2022.9833621

[43]

Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In 3rd International Symposium on NASA Formal Methods (NFM), Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.) (Lecture Notes in Computer Science, Vol. 6617). Springer, 41–55. https://doi.org/10.1007/978-3-642-20398-5_4

[44]

Koen Jacobs, Dominique Devriese, and Amin Timany. 2022. Purity of an ST monad: full abstraction by semantically typed back-translation. Proc. ACM Program. Lang., 6, OOPSLA1 (2022), 1–27. https://doi.org/10.1145/3527326

[45]

Kurt Jensen. 1978. Connection between Dijkstra’s Predicate-Transformers and Denotational Continuation-Semantics. DAIMI Report Series 7.86. http://ojs.statsbiblioteket.dk/index.php/daimipb/article/download/6502/5621

[46]

Dongyun Jin, Patrick O’Neil Meredith, Choonghwan Lee, and Grigore Roşu. 2012. JavaMOP: Efficient Parametric Runtime Monitoring Framework. In Proceeding of the 34th International Conference on Software Engineering (ICSE’12). IEEE, 1427–1430. https://doi.org/10.1109/ICSE.2012.6227231

[47]

Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2010. seL4: formal verification of an operating-system kernel. Commun. ACM, 53, 6 (2010), 107–115. https://doi.org/10.1145/1743546.1743574

[48]

Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM, 52, 7 (2009), 107–115. https://doi.org/10.1145/1538788.1538814

[49]

Thomas Letan and Yann Régis-Gianas. 2020. FreeSpec: specifying, verifying, and executing impure computations in Coq. In 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), Jasmin Blanchette and Catalin Hritcu (Eds.). ACM, 32–46. https://doi.org/10.1145/3372885.3373812

[50]

Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, and Guillaume Hiet. 2021. Modular verification of programs with effects and effects handlers. Formal Aspects Comput., 33, 1 (2021), 127–150. https://doi.org/10.1007/s00165-020-00523-2

[51]

P. Letouzey. 2008. Coq Extraction, an Overview. In LTA ’08 (Lecture Notes in Computer Science, Vol. 5028). Springer-Verlag.

[52]

Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2022. Linear Types for Large-Scale Systems Verification. In Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). https://www.andrew.cmu.edu/user/bparno/papers/linear-dafny.pdf

[53]

Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Cătălin Hriţcu, Exequiel Rivas, and Éric Tanter. 2019. Dijkstra Monads for All. Proc. ACM Program. Lang., 3, ICFP (2019), Article 104, July, 29 pages. https://doi.org/10.1145/3341708

[54]

Kenji Maillard, Cătălin Hriţcu, Exequiel Rivas, and Antoine Van Muylder. 2020. The Next 700 Relational Program Logics. PACMPL, 4, POPL (2020), 4:1–4:33. https://doi.org/10.1145/3371072

[55]

Gregory Malecha, Greg Morrisett, and Ryan Wisnesky. 2011. Trace-based verification of imperative programs with I/O. J. Symb. Comput., 46, 2 (2011), 95–118. https://doi.org/10.1016/j.jsc.2010.08.004

[56]

Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Cătălin Hriţcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, and Nikhil Swamy. 2019. Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms. In 28th European Symposium on Programming (ESOP). Springer, 30–59. https://doi.org/10.1007/978-3-030-17184-1_2

[57]

Hidehiko Masuhara, Gregor Kiczales, and Christopher Dutchyn. 2003. A Compilation and Optimization Model for Aspect-Oriented Programs. In 12th International Conference on Compiler Construction (CC), Görel Hedin (Ed.) (Lecture Notes in Computer Science, Vol. 2622). Springer, 46–60. https://doi.org/10.1007/3-540-36579-6_4

[58]

Scott Moore, Christos Dimoulas, Robert Bruce Findler, Matthew Flatt, and Stephen Chong. 2016. Extensible access control with authorization contracts. In ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Eelco Visser and Yannis Smaragdakis (Eds.). ACM, 214–233. https://doi.org/10.1145/2983990.2984021

[59]

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 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society, 415–429. isbn:978-1-4673-6166-8 https://doi.org/10.1109/SP.2013.35

[60]

Max S. New, William J. Bowman, and Amal Ahmed. 2016. Fully abstract compilation via universal embedding. In 21st ACM SIGPLAN International Conference on Functional Programming (ICFP), Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 103–116. https://doi.org/10.1145/2951913.2951941

[61]

Phuc C. Nguyen, Sam Tobin-Hochstadt, and David Van Horn. 2014. Soft contract verification. In 19th ACM SIGPLAN International Conference on Functional Programming (ICFP), Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 139–152. https://doi.org/10.1145/2628136.2628156

[62]

Peter-Michael Osera, Vilhelm Sjöberg, and Steve Zdancewic. 2012. Dependent interoperability. In 6th Workshop on Programming Languages Meets Program Verification (PLPV), Koen Claessen and Nikhil Swamy (Eds.). ACM, 3–14. https://doi.org/10.1145/2103776.2103779

[63]

Zoe Paraskevopoulou, John M. Li, and Andrew W. Appel. 2021. Compositional optimizations for CertiCoq. Proc. ACM Program. Lang., 5, ICFP (2021), 1–30. https://doi.org/10.1145/3473591

[64]

Marco Patrignani, Pieter Agten, Raoul Strackx, Bart Jacobs, Dave Clarke, and Frank Piessens. 2015. Secure Compilation to Protected Module Architectures. ACM Trans. Program. Lang. Syst., 37, 2 (2015), 6:1–6:50. https://doi.org/10.1145/2699503

[65]

Marco Patrignani, Amal Ahmed, and Dave Clarke. 2019. Formal Approaches to Secure Compilation: A survey of fully abstract compilation and related work. Comput. Surveys, https://squera.github.io/pdf/main-full.pdf

[66]

Daniel Patterson, Noble Mushtak, Andrew Wagner, and Amal Ahmed. 2022. Semantic soundness for language interoperability. In 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), Ranjit Jhala and Isil Dillig (Eds.). ACM, 609–624. https://doi.org/10.1145/3519939.3523703

[67]

Willem Penninckx, Bart Jacobs, and Frank Piessens. 2015. Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs. In 24th European Symposium on Programming (ESOP), Jan Vitek (Ed.) (Lecture Notes in Computer Science, Vol. 9032). Springer, 158–182. https://doi.org/10.1007/978-3-662-46669-8_7

[68]

Willem Penninckx, Amin Timany, and Bart Jacobs. 2019. Abstract I/O Specification. CoRR, abs/1901.10541 (2019), arXiv:1901.10541. arxiv:1901.10541

[69]

Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, and Santiago Zanella Béguelin. 2020. EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. In 2020 IEEE Symposium on Security and Privacy (SP). IEEE, 983–1002. https://doi.org/10.1109/SP40000.2020.00114

[70]

Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. 2017. Verified Low-Level Programming Embedded in F*. PACMPL, 1, ICFP (2017), Sept., 17:1–17:29. https://doi.org/10.1145/3110261

[71]

Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In 28th USENIX Security Symposium, Nadia Heninger and Patrick Traynor (Eds.). USENIX Association, 1465–1482. https://www.usenix.org/conference/usenixsecurity19/presentation/delignat-lavaud

[72]

Xiaojia Rao, Aïna Linn Georges, Maxime Legoupil, Conrad Watt, Jean Pichon-Pharabod, Philippa Gardner, and Lars Birkedal. 2023. Iris-Wasm: Robust and Modular Verification of WebAssembly Programs. Proc. ACM Program. Lang., 7, PLDI (2023), 1096–1120. https://doi.org/10.1145/3591265

[73]

Aseem Rastogi, Guido Martínez, Aymeric Fromherz, Tahina Ramananandro, and Nikhil Swamy. 2021. Programming and Proving with Indexed Effects. https://www.fstar-lang.org/papers/indexedeffects/

[74]

Michael Sammler, Simon Spies, Youngju Song, Emanuele D’Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer. 2023. DimSum: A Decentralized Approach to Multi-language Semantics and Verification. Proc. ACM Program. Lang., 7, POPL (2023), 775–805. https://doi.org/10.1145/3571220

[75]

Christophe Scholliers, Éric Tanter, and Wolfgang De Meuter. 2015. Computational contracts. Sci. Comput. Program., 98 (2015), 360–375. https://doi.org/10.1016/j.scico.2013.09.005

[76]

Lucas Silver and Steve Zdancewic. 2021. Dijkstra monads forever: termination-sensitive specifications for interaction trees. Proc. ACM Program. Lang., 5, POPL (2021), 1–28. https://doi.org/10.1145/3434307

[77]

Lau Skorstengaard, Dominique Devriese, and Lars Birkedal. 2021. StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities. J. Funct. Program., 31 (2021), e9. https://doi.org/10.1017/S095679682100006X

[78]

Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. 2020. Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proc. ACM Program. Lang., 4, POPL (2020), 8:1–8:28. https://doi.org/10.1145/3371076

[79]

Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, and Théo Winterhalter. 2023. Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. April, https://inria.hal.science/hal-04077552 working paper or preprint

[80]

Thomas Van Strydonck, Frank Piessens, and Dominique Devriese. 2021. Linear capabilities for fully abstract compilation of separation-logic-verified code. J. Funct. Program., 31 (2021), e6. https://doi.org/10.1017/S0956796821000022

[81]

Nikhil Swamy, Cătălin Hriţcu, 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. isbn:978-1-4503-3549-2 https://www.fstar-lang.org/papers/mumon/

[82]

Wouter Swierstra and Thorsten Altenkirch. 2007. Beauty in the beast. In ACM SIGPLAN Workshop on Haskell, Gabriele Keller (Ed.). ACM, 25–36. https://doi.org/10.1145/1291201.1291206

[83]

Wouter Swierstra and Tim Baanen. 2019. A predicate transformer semantics for effects (functional pearl). Proc. ACM Program. Lang., 3, ICFP (2019), 103:1–103:26. https://doi.org/10.1145/3341707

[84]

Éric Tanter. 2008. Expressive scoping of dynamically-deployed aspects. In 7th International Conference on Aspect-Oriented Software Development (AOSD), Theo D’Hondt (Ed.). ACM, 168–179. https://doi.org/10.1145/1353482.1353503

[85]

Éric Tanter and Nicolas Tabareau. 2015. Gradual certified programming in Coq. In 11th Symposium on Dynamic Languages (DLS), Manuel Serrano (Ed.). ACM, 26–40. https://doi.org/10.1145/2816707.2816710

[86]

Jesse A. Tov and Riccardo Pucella. 2010. Stateful Contracts for Affine Types. In 19th European Symposium on Programming (ESOP), Andrew D. Gordon (Ed.) (Lecture Notes in Computer Science, Vol. 6012). Springer, 550–569. https://doi.org/10.1007/978-3-642-11957-6_29

[87]

Théo Winterhalter, Cezar-Constantin Andrici, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, and Exequiel Rivas. 2022. Partial Dijkstra Monads for All. TYPES. https://types22.inria.fr/files/2022/06/TYPES_2022_paper_18.pdf

[88]

Jenna Wise, Johannes Bader, Cameron Wong, Jonathan Aldrich, Éric Tanter, and Joshua Sunshine. 2020. Gradual verification of recursive heap data structures. Proc. ACM Program. Lang., 4, OOPSLA (2020), 228:1–228:28. https://doi.org/10.1145/3428296

[89]

Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2020. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang., 4, POPL (2020), 51:1–51:32. https://doi.org/10.1145/3371119

[90]

Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, and Steve Zdancewic. 2021. Modular, compositional, and executable formal semantics for LLVM IR. Proc. ACM Program. Lang., 5, ICFP (2021), 1–30. https://doi.org/10.1145/3473572

[91]

Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. 2021. Verifying an HTTP Key-Value Server with Interaction Trees and VST. In 12th International Conference on Interactive Theorem Proving (ITP), Liron Cohen and Cezary Kaliszyk (Eds.) (LIPIcs, Vol. 193). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 32:1–32:19. https://doi.org/10.4230/LIPIcs.ITP.2021.32

[92]

Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. 2017. HACL*: A Verified Modern Cryptographic Library. In ACM Conference on Computer and Communications Security. ACM, 1789–1806. http://eprint.iacr.org/2017/536

Cited By

Thibault JBlanco RLee DArgo SAzevedo de Amorim AGeorges AHriţcu CTolmach ALuo BLiao XXu JKirda ELie D(2024)SECOMP: Formally Secure Compilation of Compartmentalized C ProgramsProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3670288(1061-1075)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3670288

Index Terms

Securing Verified IO Programs Against Unverified Code in F*
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Software verification

Recommendations

Dependent types and multi-monadic effects in F*
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

We 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 ...
Verdi: a framework for implementing and formally verifying distributed systems
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex ...
Dependent types and multi-monadic effects in F*
POPL '16

We 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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 8, Issue POPL

January 2024

2820 pages

EISSN:2475-1421

DOI:10.1145/3554315

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2024 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 January 2024

Published in PACMPL Volume 8, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

European Research Council
Deutsche Forschungsgemeinschaft
Estonian Research Council
Bundesministerium für Bildung und Forschung

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
437
Total Downloads

Downloads (Last 12 months)314
Downloads (Last 6 weeks)30

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Thibault JBlanco RLee DArgo SAzevedo de Amorim AGeorges AHriţcu CTolmach ALuo BLiao XXu JKirda ELie D(2024)SECOMP: Formally Secure Compilation of Compartmentalized C ProgramsProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3670288(1061-1075)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3670288

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents