112 citations · 260 across the 19 of their papers we have counts for
27 papers
Misquoted No More: Securely Extracting F* Programs with IO
Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman +3
Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded program…
Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
Jérémy Thibault, Joseph Lenormand, Catalin Hritcu
Researchers aim to build secure compilation chains enforcing that if there is no attack a source context can mount against a source program then there is also no attack an adversar…
SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F*
Cezar-Constantin Andrici, Danel Ahman, Catalin Hritcu +4
We introduce SecRef*, a secure compilation framework protecting stateful programs verified in F* against linked unverified code, with which the program dynamically shares ML-style…
FSLH: Flexible Mechanized Speculative Load Hardening
Jonathan Baumann, Roberto Blanco, Léon Ducruet +2
The Spectre speculative side-channel attacks pose formidable threats for security. Research has shown that code following the cryptographic constant-time discipline can be efficien…
SECOMP: Formally Secure Compilation of Compartmentalized C Programs
Jérémy Thibault, Roberto Blanco, Dongjae Lee +5
Undefined behavior in C often causes devastating security vulnerabilities. One practical mitigation is compartmentalization, which allows developers to structure large programs int…
Securing Verified IO Programs Against Unverified Code in F*
Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu +4
We introduce SCIO*, a formally secure compilation framework for statically verified partial programs performing input-output (IO). The source language is an F* subset in which a ve…
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation
Akram El-Korashy, Roberto Blanco, Jérémy Thibault +3
Proving secure compilation of partial programs typically requires back-translating an attack against the compiled program to an attack against the source program. To prove back-tra…
Dynamic IFC Theorems for Free!
Maximilian Algehed, Jean-Philippe Bernardy, Catalin Hritcu
We show that noninterference and transparency, the key soundness theorems for dynamic IFC libraries, can be obtained "for free", as direct consequences of the more general parametr…
Trace-Relating Compiler Correctness and Secure Compilation
Carmine Abate, Roberto Blanco, Stefan Ciobaca +6
Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equiva…
The Next 700 Relational Program Logics
Kenji Maillard, Catalin Hritcu, Exequiel Rivas +1
We propose the first framework for defining relational program logics for arbitrary monadic effects. The framework is embedded within a relational dependent type theory and is high…
Dijkstra Monads for All
Kenji Maillard, Danel Ahman, Robert Atkey +4
This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effects using Dijkstra monads, which we define as monad-like structures indexed…
Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation
Carmine Abate, Roberto Blanco, Deepak Garg +3
(CROPPED TO FIT IN ARXIV'S SILLY LIMIT. SEE PDF FOR COMPLETE ABSTRACT.) We are the first to thoroughly explore a large space of formal secure compilation criteria based on robust p…
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu +10
We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of tactics and metaprogramming to dischar…
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise
Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco +8
We propose a new formal criterion for evaluating secure compilation schemes for unsafe languages, expressing end-to-end security guarantees for software components that may become…
Formally Secure Compilation of Unsafe Low-Level Components (Extended Abstract)
Guglielmo Fachini, Catalin Hritcu, Marco Stronati +5
We propose a new formal criterion for secure compilation, providing strong security guarantees for components written in unsafe, low-level languages with C-style undefined behavior…
Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract)
Deepak Garg, Catalin Hritcu, Marco Patrignani +2
We map the space of soundness criteria for secure compilation based on the preservation of hyperproperties in arbitrary adversarial contexts, which we call robust hyperproperty pre…
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Catalin Hritcu +3
We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that a property witnessed in a prior state can be soundly recalled in the…
The Meaning of Memory Safety
Arthur Azevedo de Amorim, Catalin Hritcu, Benjamin C. Pierce
We give a rigorous characterization of what it means for a programming language to be memory safe, capturing the intuition that memory safety supports local reasoning about state.…
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet +7
Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diver…
Verified Low-Level Programming Embedded in F*
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi +8
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a sm…
Dijkstra Monads for Free
Danel Ahman, Catalin Hritcu, Kenji Maillard +5
Dijkstra monads enable a dependent type theory to be enhanced with support for specifying and verifying effectful code via weakest preconditions. Together with their closely relate…
Beginner's Luck: A Language for Property-Based Generators
Leonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu +3
Property-based random testing a la QuickCheck requires building efficient generators for well-distributed random data satisfying complex logical predicates, but writing these gener…
Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation
Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim +2
Compartmentalization is good security-engineering practice. By breaking a large software system into mutually distrustful components that run with minimal privileges, restricting t…
Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components
Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim +3
Secure compilation prevents all low-level attacks on compiled code and allows for sound reasoning about security in the source language. In this work we propose a new attacker mode…