Matteo Busi
ABSTRACT
Secure compilation investigates when compilation chains preserve security properties. Over the years, different formal criteria and proof techniques have been put forward for proving a compiler secure. However, these proposals require a lot of manual effort by compiler designers. This paper introduces a formal approach to mechanically support these efforts. We focus on the specific class of robust safety properties and we propose a translation validation approach that leverages program analysis techniques to check that a compilation run preserves security.
- Martín Abadi. 1999. Protection in Programming-Language Translations. In Secure Internet Programming, Security Issues for Mobile and Distributed Objects (LNCS), J. Vitek and C.D. Jensen (Eds.), Vol. 1603. Springer, 19--34.Google Scholar
- Carmine Abate, Roberto Blanco, Ştefan Ciobâcă, et al. 2020. Trace-Relating Compiler Correctness and Secure Compilation. In 29th European Symposium on Programming. 1--28.Google Scholar
- Carmine Abate, Roberto Blanco, Deepak Garg, et al. 2019. Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. In 32nd IEEE Computer Security Foundations Symposium, 2019. 256--271.Google Scholar
- Carmine Abate, Matteo Busi, and Stelios Tsampas. 2021. Fully Abstract and Robust Compilation. In Asian Symposium on Programming Languages and Systems. Springer, 83--101.Google Scholar
- Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, et al. 2018. When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. In Procs 2018 ACM SIGSAC Conference on Computer and Communications Security. 1351--1368.Google ScholarDigital Library
- Bowen Alpern and Fred B. Schneider. 1985. Defining Liveness. Inf. Process. Lett. 21, 4 (1985), 181--185.Google ScholarCross Ref
- Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, et al. 2020. Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4, POPL (2020), 7:1--7:30. Google ScholarDigital Library
- Gilles Barthe, Benjamin Grégoire, and Vincent Laporte. 2018. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time". In 31st IEEE Computer Security Foundations Symposium, 2018. 328--343.Google ScholarCross Ref
- Massimo Bartoletti, Pierpaolo Degano, and Gian Luigi Ferrari. 2005. Enforcing Secure Service Composition. In 18th IEEE Computer Security Foundations W/S. 211--223.Google Scholar
- Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari, et al. 2009. Local policies for resource usage analysis. ACM Trans. Program. Lang. Syst. 31, 6 (2009), 23:1--23:43. Google ScholarDigital Library
- Matteo Busi, Job Noorman, Jo Van Bulck, et al. 2021. Securing Interruptible Enclaved Execution on Small Microprocessors. ACM Trans. Program. Lang. Syst. 43, 3 (2021).Google ScholarDigital Library
- Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. Journal of Computer Security 18, 6 (2010), 1157--1210.Google ScholarCross Ref
- George Coker, Joshua D. Guttman, Peter Loscocco, et al. 2011. Principles of remote attestation. Int. J. Inf. Sec. 10, 2 (2011), 63--81.Google ScholarDigital Library
- Chaoqiang Deng and Kedar S. Namjoshi. 2016. Securing a Compiler Transformation. In Procs Static Analysis - 23rd International Symposium, 2016 (LNCS), X. Rival (Ed.), Vol. 9837. Springer, 170--188.Google Scholar
- Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. Semantics Engineering with PLT Redex. MIT Press.Google ScholarDigital Library
- Catalin Hritcu, David Chisnall, Deepak Garg, et al. 2019. Secure Compilation. https://blog.sigplan.org/2019/07/01/secure-compilation/. Last access Feb 2021.Google Scholar
- Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, et al. 2016. Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. In IEEE 29th Computer Security Foundations Symposium. 45--60.Google Scholar
- Leslie Lamport. 1977. Proving the Correctness of Multiprocess Programs. IEEE Trans. Software Eng. 3, 2 (1977), 125--143.Google ScholarDigital Library
- Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Procs 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006. 42--54.Google ScholarDigital Library
- Frank McKeen, Ilya Alexandrovich, Alex Berenzon, et al. 2013. Innovative instructions and software model for isolated execution. In 2nd W/S on H/W and Architectural Support for Security and Privacy, R.B. Lee and W. Shi (Eds.). ACM.Google Scholar
- Kedar S. Namjoshi and Lucas M. Tabajara. 2020. Witnessing Secure Compilation. In Procs Verification, Model Checking, and Abstract Interpretation - 21st International Conference, 2020. 1--22.Google Scholar
- Kedar S. Namjoshi and Lenore D. Zuck. 2013. Witnessing Program Transformations. In Procs Static Analysis - 20th International Symposium, 2013. 304--323.Google Scholar
- George C. Necula. 2000. Translation validation for an optimizing compiler. In Procs 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2000, M.S. Lam (Ed.). ACM, 83--94.Google ScholarDigital Library
- Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 1999. Principles of program analysis. Springer. Google ScholarCross Ref
- Job Noorman, Jo Van Bulck, Jan Tobias Mühlberg, et al. 2017. Sancus 2.0: A Low-Cost Security Architecture for IoT Devices. ACM Trans. Priv. Secur. 20, 3, Article 7 (July 2017), 33 pages. Google ScholarDigital Library
- Marco Patrignani, Amal Ahmed, and Dave Clarke. 2019. Formal Approaches to Secure Compilation: A survey of fully abstract compilation and related work. Comput. Surveys (2019).Google ScholarDigital Library
- Marco Patrignani and Deepak Garg. 2017. Secure Compilation and Hyperproperty Preservation. In 30th IEEE Computer Security Foundations Symposium. IEEE Computer Society, 392--404.Google Scholar
- Marco Patrignani and Deepak Garg. 2019. Robustly Safe Compilation. In Procs 28th European Symposium on Programming. 469--498.Google ScholarCross Ref
- Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation Validation. In Procs 4th Tools and Algorithms for Construction and Analysis of Systems, International Conference (LNCS), B. Steffen (Ed.), Vol. 1384. Springer, 151--166.Google Scholar
- Charles Reis and Steven D. Gribble. 2009. Isolating Web Programs in Modern Browser Architectures. In Procs 4th ACM European Conference on Computer Systems. ACM, 219--232. Google ScholarDigital Library
- Thomas A.L. Sewell, Magnus O. Myreen, and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In ACM SIGPLAN Conference on Programming Language Design and Implementation. 471--482.Google ScholarDigital Library
- Robert Sison and Toby Murray. 2019. Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. In 10th International Conference on Interactive Theorem Proving, J. Harrison, J. O'Leary, and A. Tolmach (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 27:1--27:19.Google Scholar
- Christian Skalka, David Darais, Trent Jaeger, et al. 2020. Types and Abstract Interpretation for Authorization Hook Advice. In CSF. IEEE, 139--152.Google Scholar
- Moshe Y. Vardi. 2007. Automata-Theoretic Model Checking Revisited. In VMCAI (LNCS), Vol. 4349. Springer, 137--150.Google Scholar
- Robert Wahbe, Steven Lucco, Thomas E. Anderson, et al. 1993. Efficient Software-Based Fault Isolation. SIGOPS Oper. Syst. Rev. 27, 5 (Dec. 1993), 203--216.Google ScholarDigital Library
Index Terms
- Towards effective preservation of robust safety properties
Index terms have been assigned to the content through auto-classification.
Recommendations
Temporal-logic property preservation under Z refinement
AbstractFormal specification languages such as Z, B and VDM are used in the incremental development of abstract specifications (suitable for establishing required properties) to more concrete specifications (resembling the final implementation). This ...
Runtime Verification of Safety-Progress Properties
Runtime VerificationThe underlying property, its definition and representation play a major role when monitoring a system. Having a suitable and convenient framework to express properties is thus a concern for runtime analysis. It is desirable to delineate in this ...
Enforcing Safety and Progress Properties: An Approach to Concurrent Program Derivation
ASWEC '09: Proceedings of the 2009 Australian Software Engineering ConferenceIn this paper we develop an approach for deriving concurrent programs. At any stage in its derivation, a program consists of a combination of the code for its processes together with a set of enforced properties. The behaviour of such a combination ...
Comments