Hostname: page-component-586b7cd67f-vdxz6 Total loading time: 0 Render date: 2024-11-22T05:49:50.709Z Has data issue: false hasContentIssue false
  • English
  • Français

Linear capabilities for fully abstract compilation of separation-logic-verified code

Part of: ICFP 2019

Published online by Cambridge University Press:  30 March 2021

THOMAS VAN STRYDONCK Open the ORCID record for THOMAS VAN STRYDONCK [Opens in a new window] ,
FRANK PIESSENS  and
DOMINIQUE DEVRIESE Open the ORCID record for DOMINIQUE DEVRIESE [Opens in a new window]
THOMAS VAN STRYDONCK
Affiliation:
KU Leuven, Leuven, Belgium, (e-mails: [email protected], [email protected])
FRANK PIESSENS
Affiliation:
KU Leuven, Leuven, Belgium, (e-mails: [email protected], [email protected])
DOMINIQUE DEVRIESE
Affiliation:
Vrije Universiteit Brussel, Brussels, Belgium, (e-mail: [email protected])
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.

Separation logic is a powerful program logic for the static modular verification of imperative programs. However, dynamic checking of separation logic contracts on the boundaries between verified and untrusted modules is hard because it requires one to enforce (among other things) that outcalls from a verified to an untrusted module do not access memory resources currently owned by the verified module. This paper proposes an approach to dynamic contract checking by relying on support for capabilities, a well-studied form of unforgeable memory pointers that enables fine-grained, efficient memory access control. More specifically, we rely on a form of capabilities called linear capabilities for which the hardware enforces that they cannot be copied. We formalize our approach as a fully abstract compiler from a statically verified source language to an unverified target language with support for linear capabilities. The key insight behind our compiler is that memory resources described by spatial separation logic predicates can be represented at run time by linear capabilities. The compiler is separation-logic-proof-directed: it uses the separation logic proof of the source program to determine how memory accesses in the source program should be compiled to linear capability accesses in the target program. The full abstraction property of the compiler essentially guarantees that compiled verified modules can interact with untrusted target language modules as if they were compiled from verified code as well. This article is an extended version of one that was presented at ICFP 2019 (Van Strydonck et al., 2019).

Type
Research Article
Information
Journal of Functional Programming , Volume 31 , 2021 , e6
Check for updates
Copyright
© The Author(s), 2021. Published by Cambridge University Press

References

Abadi, M. (1999) Protection in programming-language translations. In Secure Internet Programming. Springer-Verlag, pp. 19–34.CrossRefGoogle Scholar
Abadi, M. & Plotkin, G. D. (2012) On protection by layout randomization. ACM Trans. Inf. Syst. Secur. 15(2), 8:1–8:29.CrossRefGoogle Scholar
Agten, P., Jacobs, B. & Piessens, F. (2015) Sound modular verification of C code executing in an unverified context. In Symposium on Principles of Programming Languages. POPL’15. New York, NY, USA: ACM, pp. 581–594.Google Scholar
Bader, J., Aldrich, J. & Tanter, É. (2018) Gradual program verification. In Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science. Springer International Publishing.Google Scholar
Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P. W., Wies, T. & Yang, H. (2007) Shape analysis for composite data structures. In International Conference on Computer Aided Verification. Springer, pp. 178–192.CrossRefGoogle Scholar
Berdine, J., Calcagno, C. & O’Hearn, P. W. (2005) Smallfoot: Modular automatic assertion checking with separation logic. In Formal Methods for Components and Objects. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, pp. 115–137.Google Scholar
Berdine, J., Cook, B. & Ishtiaq, S. (2011) SLAyer: Memory safety for systems-level code. In Computer Aided Verification. Springer, pp. 178–183.CrossRefGoogle Scholar
Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O’Hearn, P., Papakonstantinou, I., Purbrick, J. & Rodriguez, D. (2015) Moving fast with software verification. In NASA Formal Methods Symposium. Springer, pp. 3–11.CrossRefGoogle Scholar
Chisnall, D., Rothwell, C., Watson, R. N. M., Woodruff, J., Vadera, M., Moore, S. W., Roe, M., Davis, B. & Neumann, P. G. (2015) Beyond the PDP-11: Architectural support for a memory-safe C abstract machine. In Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS’15, Istanbul, Turkey, March 14–18, 2015, pp. 117–130.CrossRefGoogle Scholar
Chlipala, A. (2017) Formal reasoning about programs. Available at: http://adam.chlipala.net/frap.Google Scholar
Costan, V. & Devadas, S. (2016) Intel SGX explained. IACR Cryptol. Eprint Arch. 2016(086), 1–118.Google Scholar
de Amorim, A. A., Collins, N., DeHon, A., Demange, D., Hritcu, C., Pichardie, D., Pierce, B. C., Pollack, R. & Tolmach, A. (2016). A verified information-flow architecture. J. Comput. Secur. 24(6), 689–734.CrossRefGoogle Scholar
de Amorim, A. A., Dénès, M., Giannarakis, N., Hritcu, C., Pierce, B. C., Spector-Zabusky, A. & Tolmach, A. (2015) Micro-policies: Formally verified, tag-based security monitors. In 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17–21, 2015, pp. 813–830.CrossRefGoogle Scholar
Devriese, D., Patrignani, M. & Piessens, F. (2016) Fully-abstract compilation by approximate back-translation. In Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20–22, 2016, pp. 164–177.CrossRefGoogle Scholar
Dimoulas, C., New, M. S., Findler, R. B. & Felleisen, M. (2016) Oh lord, please don’t let contracts be misunderstood (functional pearl). In International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18–22, 2016, pp. 117–131.CrossRefGoogle Scholar
Distefano, D., O’Hearn, P. W. & Yang, H. (2006) A local shape analysis based on separation logic. In Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006, Vienna, Austria, March 25–April 2, 2006, Proceedings, Hermanns, H. & Palsberg, J. (eds). Lecture Notes in Computer Science, vol. 3920. Springer, pp. 287–302.CrossRefGoogle Scholar
Fournet, C., Swamy, N., Chen, J., Dagand, P.-É., Strub, P.-Y. & Livshits, B. (2013) Fully abstract compilation to JavaScript. In Symposium on Principles of Programming Languages, POPL’13, pp. 371–384.CrossRefGoogle Scholar
Garcia, R., Clark, A. M. & Tanter, É. (2016) Abstracting gradual typing. In Principles of Programming Languages. ACM, pp. 429–442.Google Scholar
Garg, D., Hritcu, C., Patrignani, M., Stronati, M. & Swasey, D. (2017) Robust hyperproperty preservation for secure compilation (extended abstract). Available at: http://arxiv.org/abs/1710.07309.Google Scholar
Insolvibile, G. (2003) Garbage collection in C programs. Linux J. 2003(113), 7.Google Scholar
Jacobs, B. & Piessens, F. (2008) The VeriFast program verifier. Cw Reports.Google Scholar
Jacobs, B., Smans, J. & Piessens, F. (2010) A quick tour of the VeriFast program verifier. In Programming Languages and Systems. Lecture Notes in Computer Science, vol. 6461. Berlin, Heidelberg: Springer, pp. 304–311.CrossRefGoogle Scholar
Jung, R., Krebbers, R., Birkedal, L. & Dreyer, D. (2016) Higher-order ghost state. In International Conference on Functional Programming. ICFP 2016. New York, NY, USA: Association for Computing Machinery, pp. 256–269.CrossRefGoogle Scholar
Jung, R., Krebbers, R., Jourdan, J.-H., Bizjak, A., Birkedal, L. & Dreyer, D. (2018) Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20.CrossRefGoogle Scholar
Jung, R., Jourdan, J.-H., Krebbers, R. & Dreyer, D. (2018) RustBelt: Securing the foundations of the Rust programming language. Proc. ACM Program. Lang. 2(POPL), 66:1–66:34.CrossRefGoogle Scholar
Knight, T. F. Jr., DeHon, A., Sutherland, A., Dhawan, U., Kwon, A. & Ray, S. (2012) SAFE ISA (version 3.0 with interrupts per thread). Available at: http://ic.ese.upenn.edu/distributions/safe_processor/.Google Scholar
Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D. & Birkedal, L. (2017). The essence of higher-order concurrent separation logic. In Programming Languages and Systems, Yang, H. (ed). Berlin, Heidelberg: Springer, pp. 696–723.CrossRefGoogle Scholar
Leroy, X. (2006) Formal certification of a compiler back-end or: Programming a compiler with a proof assistant. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL’06. New York, NY, USA: Association for Computing Machinery, pp. 42–54.CrossRefGoogle Scholar
Leroy, X., Blazy, S., Kästner, D., Schommer, B., Pister, M. & Ferdinand, C. (2016) CompCert - a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress. SEE, Toulouse, France.Google Scholar
Levy, H. M. (1984) Capability-Based Computer Systems. Digital Press.Google Scholar
New, M. S., Bowman, W. J. & Ahmed, A. (2016) Fully abstract compilation via universal embedding. In International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18–22, 2016, pp. 103–116.CrossRefGoogle Scholar
Nguyen, H. H., Kuncak, V. & Chin, W.-N. (2008) Runtime checking for separation logic. In Verification, Model Checking, and Abstract Interpretation, 9th International Conference, pp. 203–217.CrossRefGoogle Scholar
Noorman, J., Agten, P., Daniels, W., Strackx, R., Van Herrewege, A., Huygens, C., Preneel, B., Verbauwhede, I. & Piessens, F. (2013) Sancus: Low-cost trustworthy extensible networked devices with a zero-software trusted computing base. In USENIX Security Symposium, pp. 479–494.Google Scholar
O’Hearn, P. W. (2012) A primer on separation logic (and automatic program verification and analysis). In Software Safety and Security - Tools for Analysis and Verification, pp. 286–318.Google Scholar
Patrignani, M., Agten, P., Strackx, R., Jacobs, B., Clarke, D. & Piessens, F. (2015) Secure compilation to protected module architectures. ACM Trans. Program. Lang. Syst. 37(2), 6:1–6:50.CrossRefGoogle Scholar
Patrignani, M., Ahmed, A. & Clarke, D. (2019) Formal approaches to secure compilation: A survey of fully abstract compilation and related work. ACM Comput. Surv. 51(6), 125:1–125:36.CrossRefGoogle Scholar
Patrignani, M. & Garg, D. (2017) Secure compilation and hyperproperty preservation. In Computer Security Foundations Symposium. IEEE, pp. 392–404.CrossRefGoogle Scholar
Patrignani, M. & Garg, D. (2018) Robustly safe compilation or, efficient, provably secure compilation. Corr, abs/1804.00489.Google Scholar
Pédrot, P.-M., Tabareau, N., Fehrmann, H. J. & Tanter, É. (2019) A reasonably exceptional type theory. Proc. ACM Program. Lang. 3(ICFP), 108:1–108:29.CrossRefGoogle Scholar
Pierce, B. C. (2002) Types and Programming Languages. MIT Press. Google-Books-ID: ti6zoAC9Ph8C.Google Scholar
Reynolds, J. C. (1983) Types, abstraction, and parametric polymorphism. In Information Processing. North Holland, pp. 513–523.Google Scholar
Reynolds, J. C. (2002) Separation logic: A logic for shared mutable data structures. In Logic in Computer Science. IEEE, pp. 55–74.Google Scholar
Sammler, M., Garg, D., Dreyer, D. & Litak, T. (2020) The high-level benefits of low-level sandboxing. Proc. ACM Program. Lang. 4(POPL), 32:1–32:32.CrossRefGoogle Scholar
Sieber, K. (1992) Reasoning about sequential functions via logical relations. Appl. Categories Comput. Sci. 177, 258–269.CrossRefGoogle Scholar
Skorstengaard, L., Devriese, D. & Birkedal, L. (2018) Reasoning about a machine with local capabilities. In Programming Languages and Systems, vol. 10801. Springer International Publishing, pp. 475–501.Google Scholar
Skorstengaard, L., Devriese, D. & Birkedal, L. (2019) StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities. Proc. ACM Program. Lang. 3(POPL), 19:1–19:28.CrossRefGoogle Scholar
Strackx, R., Piessens, F. & Preneel, B. (2010) Efficient isolation of trusted subsystems in embedded systems. In Security and Privacy in Communication Networks. Lecture Notes. Berlin, Heidelberg: Springer, pp. 344–361.CrossRefGoogle Scholar
Swasey, D., Garg, D. & Dreyer, D. (2017) Robust and compositional verification of object capability patterns. Proc. ACM Program. Lang. 1(OOPSLA), 89:1–89:26.CrossRefGoogle Scholar
van Ginkel, N., Strackx, R. & Piessens, F. (2017) Automatically generating secure wrappers for SGX enclaves from separation logic specifications. In Programming Languages and Systems, Chang, B.-Y. E. (ed). Cham: Springer International Publishing, pp. 105–123.CrossRefGoogle Scholar
Van Strydonck, T., Piessens, F. & Devriese, D. (2019) Linear capabilities for fully abstract compilation of separation-logic-verified code. Proc. ACM Program. Lang., ICFP.CrossRefGoogle Scholar
Van Strydonck, T., Piessens, F. & Devriese, D. (2020) Linear capabilities for fully abstract compilation of separation-logic-verified code - technical appendix including proofs and details. Available at: https://soft.vub.ac.be/dodevrie/seplogic-lincaps-tr20201130.pdf.CrossRefGoogle Scholar
Vogels, F., Jacobs, B. & Piessens, F. (2015) Featherweight VeriFast. Log. Methods Comput. Sci. 11(3), 19:1–19:57.Google Scholar
Watson, R. N. M., Neumann, P. G., Woodruff, J., Roe, M., Almatary, H., Anderson, J., Baldwin, J., Barnes, G., Chisnall, D., Clarke, J., Davis, B., Eisen, L., Filardo, N. W., Grisenthwaite, R., Joannou, A., Laurie, B., Markettos, A. T., Moore, S. W., Murdoch, S. J., Nienhuis, K., Norton, R., Richardson, A., Rugg, P., Sewell, P., Son, S. & Xia, H. (2020) Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8). Technical Report UCAM-CL-TR-951. University of Cambridge, Computer Laboratory.Google Scholar
Watson, R. N. M., Woodruff, J., Neumann, P. G., Moore, S. W., Anderson, J., Chisnall, D., Dave, N., Davis, B., Gudka, K., Laurie, B., Murdoch, S. J., Norton, R., Roe, M., Son, S., & Vadera, M. (2015) CHERI: A hybrid capability-system architecture for scalable software compartmentalization. In IEEE Symposium on Security and Privacy, pp. 20–37.CrossRefGoogle Scholar
Supplementary material: PDF

Van Strydonck et al. supplementary material

Van Strydonck et al. supplementary material

Download Van Strydonck et al. supplementary material(PDF)
PDF 1.3 MB
Submit a response

Discussions

No Discussions have been published for this article.