Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

26 résultats
Page :
triés par
Image document

Micro-Policies: Formally Verified, Tag-Based Security Monitors

 Arthur Azevedo de Amorim , Maxime Dénès , Nick Giannarakis , Cătălin Hriţcu , Benjamin C. Pierce , et al.
2015 IEEE Symposium on Security and Privacy, May 2015, San Jose, United States. pp.813 - 830, ⟨10.1109/SP.2015.55⟩
Communication dans un congrès hal-01265666v1

The Meaning of Memory Safety

 Arthur Azevedo de Amorim , Cătălin Hriţcu , Benjamin C. Pierce
7th International Conference on Principles of Security and Trust (POST), Apr 2018, Thessaloniki, Greece. pp.79--105, ⟨10.1007/978-3-319-89722-6_4⟩
Communication dans un congrès hal-01949201v1

Verified Low‐Level Programming Embedded in F*

 Jonathan Protzenko , Jean‐karim Zinzindohoué , Aseem Rastogi , Tahina Ramananandro , Peng Wang , et al.
Proceedings of the ACM on Programming Languages, 2017, 1 (ICFP), pp.17:1--17:29. ⟨10.1145/3110261⟩
Article dans une revue hal-01672706v1

Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation

 Yannis Juglaret , Cătălin Hriţcu , Arthur Azevedo De Amorim , Boris Eng , Benjamin C. Pierce
29th IEEE Symposium on Computer Security Foundations (CSF), 2016, Lisabon, Portugal. pp.45--60, ⟨10.1109/CSF.2016.11⟩
Communication dans un congrès hal-01424795v1

Meta-F*: Proof automation with SMT, Tactics, and Metaprograms

 Guido Martínez , Danel Ahman , Victor Dumitrescu , Nick Giannarakis , Chris Hawblitzel , et al.
ESOP'19 - European Symposium on Programming, Apr 2019, Prague, Czech Republic. ⟨10.1007/978-3-030-17184-1_2⟩
Communication dans un congrès hal-01995376v1
Image document

Dependent Types and Multi-Monadic Effects in F*

 Nikhil Swamy , Cătălin Hriţcu , Chantal Keller , Aseem Rastogi , Antoine Delignat-Lavaud , et al.
43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016, St. Petersburg, Florida, United States. pp.256-270, ⟨10.1145/2837614.2837655⟩
Communication dans un congrès hal-01265793v1

Testing Noninterference, Quickly

 Cătălin Hriţcu , Leonidas Lampropoulos , Antal Spector-Zabusky , Arthur Azevedo de Amorim , Maxime Dénès , et al.
[Research Report] arXiv:1409.0393, arXiv. 2014, pp.50
Rapport hal-01102224v1
Image document

Recalling a Witness: Foundations and Applications of Monotonic State

 Danel Ahman , Cédric Fournet , Cătălin Hriţcu , Kenji Maillard , Aseem Rastogi , et al.
Proceedings of the ACM on Programming Languages, 2018, 2 (POPL), ⟨10.1145/3158153⟩
Article dans une revue hal-01672733v1
Image document

The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography

 Philipp G Haselwarter , Benjamin Salling Hvass , Lasse Letager Hansen , Théo Winterhalter , Cătălin Hriţcu , et al.
CPP 2024 - 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2024, London, United Kingdom. pp.30-44, ⟨10.1145/3636501.3636961⟩
Communication dans un congrès hal-04484598v1

Dijkstra Monads for Free

 Danel Ahman , Cătălin Hriţcu , Kenji Maillard , Guido Martínez , Gordon Plotkin , et al.
44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017, Paris, France. pp.515-529, ⟨10.1145/3009837.3009878⟩
Communication dans un congrès hal-01424794v1

A Monadic Framework for Relational Verification

 Niklas Grimm , Kenji Maillard , Cédric Fournet , Cătălin Hriţcu , Matteo Maffei , et al.
7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), Jan 2018, Los Angeles, United States. pp.130--145, ⟨10.1145/3167090⟩
Communication dans un congrès hal-01672703v1
Image document

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

 Philipp Haselwarter , Exequiel Rivas , Antoine van Muylder , Théo Winterhalter , Carmine Abate , et al.
ACM Transactions on Programming Languages and Systems (TOPLAS), 2023, 45 (3), pp.1-61. ⟨10.1145/3594735⟩
Article dans une revue hal-04273257v1
Image document

The Quest for Formally Secure Compartmentalizing Compilation

 Cătălin Hriţcu
Programming Languages [cs.PL]. ENS Paris; PSL Research University, 2019
HDR tel-01995823v1

Testing Noninterference, Quickly

 Cătălin Hriţcu , Leonidas Lampropoulos , Antal Spector-Zabusky , Arthur Azevedo De Amorim , Maxime Dénès , et al.
Journal of Functional Programming, 2016, 26, e4 (62 p.). ⟨10.1017/S0956796816000058⟩
Article dans une revue hal-01424796v1
Image document

Foundational Property-Based Testing

 Zoe Paraskevopoulou , Cătălin Hriţcu , Maxime Dénès , Leonidas Lampropoulos , Benjamin C. Pierce
ITP 2015 - 6th conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_22⟩
Communication dans un congrès hal-01162898v1

A Verified Information-Flow Architecture

 Arthur Azevedo de Amorim , Nathan Collins , André Dehon , Delphine Demange , Catalin Hritcu , et al.
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014, San Diego, CA, United States. ⟨10.1145/2535838.2535839⟩
Communication dans un congrès hal-00918847v1

A Verified Information-Flow Architecture

 Arthur Azevedo de Amorim , Nathan Collins , André Dehon , Delphine Demange , Cătălin Hriţcu , et al.
Journal of Computer Security, 2016, 24 (6), pp.689--734. ⟨10.3233/JCS-15784⟩
Article dans une revue hal-01424797v1

Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations

 Michael Backes , Cătălin Hriţcu , Matteo Maffei
Journal of Computer Security, 2014, 22 (2), pp.301-353. ⟨10.3233/JCS-130493⟩
Article dans une revue hal-01102192v1
Image document

Securing Verified IO Programs Against Unverified Code in F*

 Cezar-Constantin Andrici , Ștefan Ciobâcă , Cătălin Hriţcu , Guido Martínez , Exequiel Rivas , et al.
Proceedings of the ACM on Programming Languages, 2024, 8 (POPL), pp.2226-2259. ⟨10.1145/3632916⟩
Article dans une revue hal-04484770v1

Dijkstra monads for all

 Kenji Maillard , Danel Ahman , Robert Atkey , Guido Martínez , Cătălin Hriţcu , et al.
Proceedings of the ACM on Programming Languages, 2019, 3 (ICFP), pp.1-29. ⟨10.1145/3341708⟩
Article dans une revue hal-02398919v1

Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation

 Carmine Abate , Roberto Blanco , Deepak Garg , Catalin Hritcu , Marco Patrignani , et al.
CSF 2019 - 32nd IEEE Computer Security Foundations Symposium, Jun 2019, Hoboken, United States. pp.256-271, ⟨10.1109/CSF.2019.00025⟩
Communication dans un congrès hal-02398915v1

Architectural Support for Software-Defined Metadata Processing

 Udit Dhawan , Cătălin Hriţcu , Rafi Rubin , Nikos Vasilakis , Silviu Chiricescu , et al.
20th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2015), Mar 2015, Istanbul, Turkey. pp.487-502, ⟨10.1145/2694344.2694383⟩
Communication dans un congrès hal-01102378v1
Image document

The Next 700 Relational Program Logics

 Kenji Maillard , Catalin Hritcu , Exequiel Rivas , Antoine van Muylder
Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), ⟨10.1145/3371072⟩
Article dans une revue hal-02398927v1

When Good Components Go Bad

 Carmine Abate , Arthur Azevedo de Amorim , Roberto Blanco , Ana Nora Evans , Guglielmo Fachini , et al.
25th ACM Conference on Computer and Communications Security (CCS), Oct 2018, Toronto, Canada. pp.1351--1368, ⟨10.1145/3243734.3243745⟩
Communication dans un congrès hal-01949202v1

Beginner's Luck: A Language for Random Generators

 Leonidas Lampropoulos , Diane Gallois-Wong , Cătălin Hriţcu , John Hughes , Benjamin C. Pierce , et al.
44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017, Paris, France. pp.114-129, ⟨10.1145/3009837.3009868⟩
Communication dans un congrès hal-01424793v1

Everest: Towards a Verified, Drop‐in Replacement of HTTPS

 Karthikeyan Bhargavan , Barry Bond , Antoine Delignat‐lavaud , Cédric Fournet , Chris Hawblitzel , et al.
2nd Summit on Advances in Programming Languages (SNAPL), May 2017, Asilomar, CA, United States. ⟨10.4230/LIPIcs.SNAPL.2017.1⟩
Communication dans un congrès hal-01672707v1
Page :