Fetching the paper…
Reading the bibliography…
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.
Security policies and security models
J. A. Goguen and J. Meseguer · 1982
Earlier work this paper cites.
Abstract models of memory management
G. Morrisett, M. Felleisen, and R. Harper · 1995
Earlier work this paper cites.
ISO C standard 1999
ISO · 1999
Earlier work this paper cites.
Separation logic: A logic for shared mutable data structures
J. C. Reynolds · 2002
Earlier work this paper cites.
A semantic basis for local reasoning
H. Yang and P. W. O’Hearn · 2002
Earlier work this paper cites.
CCured: type-safe retrofitting of legacy software
G. C. Necula, J. Condit, M. Harren, S. McPeak, and W. Weimer · 2005
Earlier work this paper cites.
Safe manual memory management in Cyclone
N. Swamy, M. W. Hicks, G. Morrisett, D. Grossman, and T. Jim · 2006
Earlier work this paper cites.
L 3 {}^{\mbox{3}} : A linear language with locations
A. Ahmed, M. Fluet, and G. Morrisett · 2007
Earlier work this paper cites.
Effective memory protection using dynamic tainting
J. A. Clause, I. Doudalis, A. Orso, and M. Prvulovic · 2007
Earlier work this paper cites.
Termination-insensitive noninterference leaks more than just a bit
A. Askarov, S. Hunt, A. Sabelfeld, and D. Sands · 2008
Earlier work this paper cites.
HardBound: Architectural support for spatial safety of the C programming language
J. Devietti, C. Blundell, M. M. K. Martin, and S. Zdancewic · 2008
Earlier work this paper cites.
Formal verification of a C-like memory model and its uses for verifying program transformations
X. Leroy and S. Blazy · 2008
Earlier work this paper cites.
Automatic discovery and quantification of information leaks
M. Backes, B. Köpf, and A. Rybalchenko · 2009
Earlier work this paper cites.
Compiling functional types to relational specifications for low level imperative code
N. Benton and N. Tabareau · 2009
Earlier work this paper cites.
SoftBound: highly compatible and complete spatial memory safety for C
S. Nagarakatte, J. Zhao, M. M. K. Martin, and S. Zdancewic · 2009
Earlier work this paper cites.
On the foundations of quantitative information flow
G. Smith · 2009
Earlier work this paper cites.
Object capabilities and isolation of untrusted web applications
S. Maffeis, J. C. Mitchell, and A. Taly · 2010
Earlier work this paper cites.
Conscript: Specifying and enforcing fine-grained security policies for javascript in the browser
L. A. Meyerovich and V. B. Livshits · 2010
Cited alongside, same era.
CETS: compiler enforced temporal safety for C
S. Nagarakatte, J. Zhao, M. M. K. Martin, and S. Zdancewic · 2010
Cited alongside, same era.
Automated analysis of security-critical javascript apis
A. Taly, Ú. Erlingsson, J. C. Mitchell, M. S. Miller, and J. Nagra · 2011
Cited alongside, same era.
Caja. Attack vectors for privilege escalation , 2012
2012
Cited alongside, same era.
Memento: Learning secrets from process footprints
S. Jana and V. Shmatikov · 2012
Cited alongside, same era.
Language-based control and mitigation of timing channels
D. Zhang, A. Askarov, and A. C. Myers · 2012
Cited alongside, same era.
Modular protections against non-control data attacks
C. Schlesinger, K. Pattabiraman, N. Swamy, D. Walker, and B. G. Zorn · 2014
Later among the works it cites.
Dynamic space limits for Haskell
E. Z. Yang and D. Mazières · 2014
Later among the works it cites.
Sound modular verification of C code executing in an unverified context
P. Agten, B. Jacobs, and F. Piessens · 2015
Later among the works it cites.
Micro-policies: Formally verified, tag-based security monitors
A. Azevedo de Amorim, M. Dénès, N. Giannarakis, C. Hriţcu, B. C. Pierce, A. Spector-Zabusky, and A. Tolmach · 2015
Later among the works it cites.
Beyond the PDP-11: Architectural support for a memory-safe C abstract machine
D. Chisnall, C. Rothwell, R. N. M. Watson, J. Woodruff, M. Vadera, S. W. Moore, M. Roe, B. Davis, and P. G. Neumann · 2015
Later among the works it cites.
Architectural support for software-defined metadata processing
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Defensive JavaScript - building and verifying secure web components
K. Bhargavan, A. Delignat-Lavaud, and S. Maffeis · 2013
Cited alongside, same era.
Fully abstract compilation to JavaScript
C. Fournet, N. Swamy, J. Chen, P.-É. Dagand, P.-Y. Strub, and B. Livshits · 2013
Cited alongside, same era.
Low-fat pointers: compact encoding and efficient gate-level implementation of fat pointers for spatial safety and capability-based security
A. Kwon, U. Dhawan, J. M. Smith, T. F. Knight, Jr., and A. DeHon · 2013
Cited alongside, same era.
Nominal Sets: Names and Symmetry in Computer Science
A. M. Pitts · 2013
Cited alongside, same era.
Programming with permissions in Mezzo
F. Pottier and J. Protzenko · 2013
Cited alongside, same era.
Eliminating cache-based timing attacks with instruction-based scheduling
D. Stefan, P. Buiras, E. Z. Yang, A. Levy, D. Terei, A. Russo, and D. Mazières · 2013
Cited alongside, same era.
U. Dhawan, C. Hriţcu, R. Rubin, N. Vasilakis, S. Chiricescu, J. M. Smith, T. F. Knight, Jr., B. C. Pierce, and A. DeHon · 2015
Later among the works it cites.
Guilt free Ivory
T. Elliott, L. Pike, S. Winwood, P. C. Hickey, J. Bielman, J. Sharp, E. L. Seidel, and J. Launchbury · 2015
Later among the works it cites.
A formal C memory model supporting integer-pointer casts
J. Kang, C. Hur, W. Mansky, D. Garbuzov, S. Zdancewic, and V. Vafeiadis · 2015
Later among the works it cites.
The C standard formalized in Coq
R. Krebbers · 2015
Later among the works it cites.
Oracle’s Larry Ellison claims his Sparc M7 chip is hacker-proof – errr…
C. Williams · 2015
Later among the works it cites.
A verified information-flow architecture
A. A. de Amorim, N. Collins, A. DeHon, D. Demange, C. Hritcu, D. Pichardie, B. C. Pierce, R. Pollack, and A. Tolmach · 2016
Later among the works it cites.
Reasoning about object capabilities with logical relations and effect parametricity
D. Devriese, F. Piessens, and L. Birkedal · 2016
Later among the works it cites.
Into the depths of C: elaborating the de facto standards
K. Memarian, J. Matthiesen, J. Lingard, K. Nienhuis, D. Chisnall, R. N. M. Watson, and P. Sewell · 2016
Later among the works it cites.
http://www.rust-lang.org , 2017
The Rust programming language · 2017
Closest in time.
Robust and compositional verification of object capability patterns
D. Swasey, D. Garg, and D. Dreyer · 2017
Closest in time.
Rust: from POPL to practice (keynote)
A. Turon · 2017
Closest in time.