Zobrazeno 1 - 10
of 55
pro vyhledávání: '"HRIŢCU, CĂTĂLIN"'
Autor:
Thibault, Jérémy, Blanco, Roberto, Lee, Dongjae, Argo, Sven, de Amorim, Arthur Azevedo, Georges, Aïna Linn, Hritcu, Catalin, Tolmach, Andrew
Undefined behavior in C often causes devastating security vulnerabilities. One practical mitigation is compartmentalization, which allows developers to structure large programs into mutually distrustful compartments with clearly specified privileges
Externí odkaz:
http://arxiv.org/abs/2401.16277
Autor:
Andrici, Cezar-Constantin, Ciobaca, Stefan, Hritcu, Catalin, Martínez, Guido, Rivas, Exequiel, Tanter, Éric, Winterhalter, Théo
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 verified program interacts with its IO-performing context via a higher-o
Externí odkaz:
http://arxiv.org/abs/2303.01350
Autor:
El-Korashy, Akram, Blanco, Roberto, Thibault, Jérémy, Durier, Adrien, Garg, Deepak, Hritcu, Catalin
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-translation, one can syntactically translate the target attacker to a sou
Externí odkaz:
http://arxiv.org/abs/2110.01439
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 parametricity theorem of type abstraction. This allows us to give very short s
Externí odkaz:
http://arxiv.org/abs/2005.04722
Autor:
Abate, Carmine, Blanco, Roberto, Ciobaca, Stefan, Durier, Adrien, Garg, Deepak, Hritcu, Catalin, Patrignani, Marco, Tanter, Éric, Thibault, Jérémy
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 equivalent to the preservation of all trace properties. Here traces collect,
Externí odkaz:
http://arxiv.org/abs/1907.05320
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 highly expressive. At the semantic level, we provide an algebraic presenta
Externí odkaz:
http://arxiv.org/abs/1907.05244
Autor:
Maillard, Kenji, Ahman, Danel, Atkey, Robert, Martinez, Guido, Hritcu, Catalin, Rivas, Exequiel, Tanter, Éric
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 by a specification monad. We prove that any monad morphism between a c
Externí odkaz:
http://arxiv.org/abs/1903.01237
Autor:
Abate, Carmine, Blanco, Roberto, Garg, Deepak, Hritcu, Catalin, Patrignani, Marco, Thibault, Jérémy
(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 property preservation, i.e., the preservation of properties satisfied a
Externí odkaz:
http://arxiv.org/abs/1807.04603
Autor:
Martínez, Guido, Ahman, Danel, Dumitrescu, Victor, Giannarakis, Nick, Hawblitzel, Chris, Hritcu, Catalin, Narasimhamurthy, Monal, Paraskevopoulou, Zoe, Pit-Claudel, Clément, Protzenko, Jonathan, Ramananandro, Tahina, Rastogi, Aseem, Swamy, Nikhil
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 discharge assertions not solvable by SMT, or to just simplify them into well-
Externí odkaz:
http://arxiv.org/abs/1803.06547
Autor:
Abate, Carmine, de Amorim, Arthur Azevedo, Blanco, Roberto, Evans, Ana Nora, Fachini, Guglielmo, Hritcu, Catalin, Laurent, Théo, Pierce, Benjamin C., Stronati, Marco, Thibault, Jérémy, Tolmach, Andrew
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 compromised after encountering undefined behavior---for example, by ac
Externí odkaz:
http://arxiv.org/abs/1802.00588