Fetching the paper…
Reading the bibliography…
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries.
Towards a Mathematical Science of Computation. In IFIP Congress . 21–28
John McCarthy. 1962 · 1962
Earlier work this paper cites.
Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In Advances in Cryptology – CRYPTO 1996 . Springer, 104–113
Paul C. Kocher. 1996 · 1996
Earlier work this paper cites.
Analysis of the SSL 3.0 Protocol. In 2nd USENIX Workshop on Electronic Commerce, WOEC 1996 . 29–40
David Wagner and Bruce Schneier. 1996 · 1996
Earlier work this paper cites.
Region-Based Memory Management
Mads Tofte and Jean-Pierre Talpin. 1997 · 1997
Earlier work this paper cites.
Reconsidering Custom Memory Allocation. In Proceedings of the 17th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA 2002 . ACM, 1–12
Emery D. Berger, Benjamin G. Zorn, and Kathryn S. McKinley. 2002 · 2002
Earlier work this paper cites.
Cyclone: A Safe Dialect of C.. In USENIX Annual Technical Conference, General Track . 275–288
Trevor Jim, J Gregory Morrisett, Dan Grossman, Michael W Hicks, James Cheney, and Yanling Wang. 2002 · 2002
Earlier work this paper cites.
A new extraction for Coq
Pierre Letouzey. 2002 · 2002
Earlier work this paper cites.
Exploit for CVS double free() for Linux pserver
I. Dobrovitski. 2003 · 2003
Earlier work this paper cites.
Beyond Stack Smashing: Recent Advances in Exploiting Buffer Overruns
Jonathan D. Pincus and Brandon Baker. 2004 · 2004
Earlier work this paper cites.
The Poly1305-AES message-authentication code. In International Workshop on Fast Software Encryption . Springer, 32–49
Daniel J Bernstein. 2005 · 2005
Earlier work this paper cites.
The Program Counter Security Model: Automatic Detection and Removal of Control-flow Side Channel Attacks. In 8th International Conference on Information Security and Cryptology, ICISC 2005 . Springer, 156–168
David Molnar, Matt Piotrowski, David Schultz, and David Wagner. 2006 · 2005
Earlier work this paper cites.
Curve25519: new Diffie-Hellman speed records. In International Workshop on Public Key Cryptography . Springer, 207–228
Daniel J Bernstein. 2006 · 2006
Earlier work this paper cites.
Verification of sequential imperative programs in Isabelle-HOL
Norbert Schirmer. 2006 · 2006
Earlier work this paper cites.
Dangling Pointer – Smashing The Pointer For Fun And Profit
J. Afek and A. Sharabani. 2007 · 2007
Earlier work this paper cites.
Dependent types for low-level programming. In European Symposium on Programming . Springer, 520–535
Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George C Necula. 2007 · 2007
Earlier work this paper cites.
The Salsa20 family of stream ciphers
Daniel J Bernstein. 2008 · 2008
Earlier work this paper cites.
Z3: An Efficient SMT Solver. In 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS (Lecture Notes in Computer Science) , Vol. 4963. Springer, 337–340
Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008 · 2008
Earlier work this paper cites.
Formal verification of a C-like memory model and its uses for verifying program transformations
Xavier Leroy and Sandrine Blazy. 2008 · 2008
Earlier work this paper cites.
Extraction in Coq: An Overview. In 4th Conference on Computability in Europe (Lecture Notes in Computer Science) , Vol. 5028. Springer, 359–369
Pierre Letouzey. 2008 · 2008
Earlier work this paper cites.
Mechanized semantics for the Clight subset of the C language
Sandrine Blazy and Xavier Leroy. 2009 · 2009
Earlier work this paper cites.
VCC: A practical system for verifying concurrent C. In International Conference on Theorem Proving in Higher Order Logics . Springer, 23–42
Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009 · 2009
Earlier work this paper cites.
seL4: Formal Verification of an OS Kernel. In Proceedings of the Symposium on Operating Systems Principles . ACM, 207–220
G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. 2009 · 2009
Earlier work this paper cites.
Formal verification of a realistic compiler
Xavier Leroy. 2009 · 2009
Earlier work this paper cites.
Mind the Gap. In 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009 (Lecture Notes in Computer Science) , Vol. 5674. Springer, 500–515
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, and Michael Norrish. 2009 · 2009
Earlier work this paper cites.
Here Come The ⊕ \oplus Ninjas
Thai Duong and Juliano Rizzo. 2011 · 2011
Earlier work this paper cites.
The security impact of a new cryptographic library. In International Conference on Cryptology and Information Security in Latin America, LATINCRYPT 2012 . Springer, 159–176
Daniel J Bernstein, Tanja Lange, and Peter Schwabe. 2012 · 2012
Earlier work this paper cites.
Operational Refinement for Compiler Correctness
Robert W. Dockins. 2012 · 2012
Earlier work this paper cites.
Bridging the Gap: Automatic Verified Abstraction of C. In 3rd International Conference on Interactive Theorem Proving, ITP 2012 (Lecture Notes in Computer Science) , Vol. 7406. Springer, 99–115
David Greenaway, June Andronick, and Gerwin Klein. 2012 · 2012
Earlier work this paper cites.
The CompCert Memory Model, Version 2
Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. 2012 · 2012
Earlier work this paper cites.
The CRIME Attack
Julian Rizzo and Thai Duong. 2012 · 2012
Cited alongside, same era.
Formalizing the LLVM intermediate representation for verified program transformations. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . 427–440
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. 2012 · 2012
Cited alongside, same era.
Lucky Thirteen: Breaking the TLS and DTLS Record Protocols. In 2013 IEEE Symposium on Security and Privacy . 526–540
Nadhem J. AlFardan and Kenneth G. Paterson. 2013 · 2013
Cited alongside, same era.
Implementing TLS with verified cryptographic security. In IEEE Symposium on Security and Privacy . 445–459
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, and P Strub. 2013 · 2013
Cited alongside, same era.
The Bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier. In ACM SIGPLAN Notices , Vol. 48. ACM, 391–402
Adam Chlipala. 2013 · 2013
On the Practical (In-)Security of 64-bit Block Ciphers: Collision Attacks on HTTP over TLS and OpenVPN
Karthikeyan Bhargavan and Gaëtan Leurent. 2016 · 2016
Later among the works it cites.
Wrong results with Poly1305 functions
Hanno Böck. 2016 · 2016
Later among the works it cites.
Nonce-Disrespecting Adversaries: Practical Forgery Attacks on GCM in TLS
Hanno Böck, Aaron Zauner, Sean Devlin, Juraj Somorovsky, and Philipp Jovanovic. 2016 · 2016
Later among the works it cites.
Toward compositional verification of interruptible OS kernels and device drivers. In 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016 . 431–447
Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, and Ronghui Gu. 2016 · 2016
Later among the works it cites.
Part one: Verifying s2n HMAC with SAW
Joey Dodds. 2016 · 2016
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
SoK: Eternal War in Memory. In IEEE Symposium on Security and Privacy . IEEE Computer Society, 48–62
Laszlo Szekeres, Mathias Payer, Tao Wei, and Dawn Song. 2013 · 2013
Cited alongside, same era.
Formal verification of SSA-based optimizations for LLVM. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) . 175–186
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. 2013 · 2013
Cited alongside, same era.
System-level Non-interference for Constant-time Cryptography. In 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS 2014 . 1267–1279
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Daniel Luna, and David Pichardie. 2014 · 2014
Cited alongside, same era.
TweetNaCl: A crypto library in 100 tweets. In International Conference on Cryptology and Information Security in Latin America, LATINCRYPT 2014 . 64–83
Daniel J Bernstein, Bernard Van Gastel, Wesley Janssen, Tanja Lange, Peter Schwabe, and Sjaak Smetsers. 2014 · 2014
Cited alongside, same era.
Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. In 2014 IEEE Symposium on Security and Privacy . 98–113
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, , Alfredo Pironti, and Pierre-Yves Strub. 2014a · 2014
Cited alongside, same era.
Proving the TLS handshake secure (as it is)
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, and Santiago Zanella-Béguelin. 2014b · 2014
Cited alongside, same era.
Verifying curve25519 software. In ACM SIGSAC Conference on Computer and Communications Security (CCS) . 299–309
Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, and Shang-Yi Yang. 2014 · 2014
Cited alongside, same era.
Xavier Leroy. 2004–2016 · 2016
Later among the works it cites.
Everest: VERifiEd Secure Transport
Microsoft Research and INRIA. 2016 · 2016
Later among the works it cites.
Systematic fuzzing and testing of TLS libraries. In 23rd ACM Conference on Computer and Communications Security, CCS 2016
Juraj Somorovsky. 2016 · 2016
Later among the works it cites.
Freestart Collision for Full SHA-1. In Advances in Cryptology – EUROCRYPT 2016 . Springer, 459–483
Marc Stevens, Pierre Karpman, and Thomas Peyrin. 2016 · 2016
Later among the works it cites.
Dependent Types and Multi-Monadic Effects in F*. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . ACM, 256–270
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. 2016 · 2016
Later among the works it cites.
ChaCha20/Poly1305 heap-buffer-overflow
Robert Święcki. 2016 · 2016
Later among the works it cites.
Extending C with bounds safety
David Tarditi. 2016 · 2016
Later among the works it cites.
Automated Verification of Real-World Cryptographic Implementations
A. Tomb. 2016 · 2016
Later among the works it cites.
A Verified Extensible Library of Elliptic Curves. In IEEE Computer Security Foundations Symposium (CSF)
Jean Karim Zinzindohoué, Evmorfia-Iro Bartzia, and Karthikeyan Bhargavan. 2016 · 2016
Later among the works it cites.
The Sodium crypto library (libsodium)
2008–2017 · 2017
Closest in time.
The Rust Programming Language
2010–2017 · 2017
Closest in time.
Common Weakness Enumeration (CWE-190: Integer Overflow or Wraparound)
2017 · 2017
Closest in time.
Common Weakness Enumeration (CWE-415: Double Free)
2017 · 2017
Closest in time.
Common Weakness Enumeration (CWE-416: Use After Free)
2017 · 2017
Closest in time.
Dijkstra Monads for Free. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) . ACM, 515–529
Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. 2017 · 2017
Closest in time.
LMS-Verify: Abstraction without Regret for Verified Systems Programming
Nada Amin and Tiark Rompf. 2017 · 2017
Closest in time.
Implementing and Proving the TLS 1.3 Record Layer
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin, and Jean Karim Zinzindohoue. 2017 · 2017
Closest in time.
Vale: Verifying High-Performance Cryptographic Assembly Code. In Proceedings of the USENIX Security Symposium
Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. 2017 · 2017
Closest in time.
nocrypto: OCaml cryptographic library
nocrypto. 2014–2017 · 2017
Closest in time.
OpenSSL: Cryptography and SSL/TLS Toolkit
OpenSSL library. 1998–2017 · 2017
Closest in time.
The KreMLin compiler
Jonathan Protzenko. 2017 · 2017
Closest in time.
HACL*: A Verified Modern Cryptographic Library. In ACM Conference on Computer and Communications Security . ACM, 1789–1806
Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. 2017 · 2017
Closest in time.
HACL*: A Verified Modern Cryptographic Library
Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, and Benjamin Beurdouche. 2017 · 2017
Closest in time.