diff --git a/01paper.pdf b/01paper.pdf index 68d1731..714f7d9 100644 Binary files a/01paper.pdf and b/01paper.pdf differ diff --git a/01paper.tex b/01paper.tex index 28a6b36..1564b42 100644 --- a/01paper.tex +++ b/01paper.tex @@ -89,6 +89,14 @@ vulnerabilities or at least application crashes. (might not protect against e.g.\ vtable overrides, PLT address changes, \dots) + \item Dependent types for low-level programming\cite{Dep2007} + + \item StackGuard: Automatic Adaptive Detection and Prevention of + Buffer-Overflow Attachs\cite{Stackguard1998} (ineffective in combination + with information leaks) + + \item Type-Assisted Dynamic Buffer Overflow Detection\cite{TypeAssisted2002} + \end{itemize} @@ -109,8 +117,9 @@ text \item Static analysis - \item Dependent types (only allow indexing with values that are provably in - bounds) + \item Dependent types (only allow indexing with values that are proven to be + in bounds) + \end{itemize} \subsection{Discussion}\label{ref:discussion} diff --git a/bibliography.bib b/bibliography.bib index 6a09307..fd6301d 100644 --- a/bibliography.bib +++ b/bibliography.bib @@ -1,3 +1,12 @@ +own: + +@inproceedings{TypeAssisted2002, + author = {Lhee, Kyung-suk and Chapin, Steve J.}, + booktitle = {11th USENIX Security Symposium}, + title = {{Type-Assisted Dynamic Buffer Overflow Detection}}, + year = {2002} +} + @inproceedings{Rad2001, author = {Chiueh, Tzi-cker and Hsu, Fu-Hau}, booktitle = {Proceedings 21st International Conference on Distributed Computing Systems}, @@ -5,6 +14,35 @@ title = {{RAD: A Compile-Time Solution to Buffer Overflow Attacks}}, year = {2001} } +@inproceedings{Stackguard1998, + author = {Cowan, Crispan and Po, Calton and Maier, Dave and Walpole, Jonathan + and Bakke, Peat and Beattie, Steve and Grier, Aaron and Wagle, Perru and + Yhang, Qian}, + booktitle = {7th USENIX Security Symposium}, + title = {{StackGuard: Automatic Adaptive Detection and Prevention of + Buffer-Overflow Attacks}}, + year = {1998} +} + +@InProceedings{Dep2007, +author={Condit, Jeremy +and Harren, Matthew +and Anderson, Zachary +and Gay, David +and Necula, George C.}, +editor={De Nicola, Rocco}, +title={Dependent Types for Low-Level Programming}, +booktitle={Programming Languages and Systems}, +year={2007}, +publisher={Springer Berlin Heidelberg}, +address={Berlin, Heidelberg}, +pages={520--535}, +abstract={In this paper, we describe the key principles of a dependent type system for low-level imperative languages. The major contributions of this work are (1) a sound type system that combines dependent types and mutation for variables and for heap-allocated structures in a more flexible way than before and (2) a technique for automatically inferring dependent types for local variables. We have applied these general principles to design Deputy, a dependent type system for C that allows the user to describe bounded pointers and tagged unions. Deputy has been used to annotate and check a number of real-world C programs.}, +isbn={978-3-540-71316-6} +} + +existing: + @article{Laprie2004, author = {Avizienis, Algirdas and Laprie, Jean-Claude and Randell, Brian and Landwehr, Carl}, journal = {IEEE Transactions on Dependable and Secure Computing},