Appendix E Annotated Bibliography
All of these papers are available at http://www.splint.org/publications/.
[Barker01] Chris Barker. Static Error Checking of C Applications Ported from UNIX to WIN32 Systems Using LCLint. Senior Thesis, University of Virginia Deptartment of Computer Science. May 2001.
Describes annotations and checks useful for porting applications.
[Evans94] David Evans. Using specifications to check source code. MIT/LCS/TR 628, Laboratory for Computer Science, MIT, June 1994.
MIT SM Thesis. Describes research behind Splint, focusing on how specifications can be exploited to do lightweight checking. Includes case studies using LCLint.
[EGHT94] David Evans, John Guttag, Jim Horning and Yang Meng Tan. LCLint: A tool for using specifications to check code. SIGSOFT Symposium on the Foundations of Software Engineering, December 1994.
Somewhat obsolete introduction to LCLint. Shows how LCLint is used to find errors in a sample program.
[Evans96] David Evans. Static Detection of Dynamic Memory Errors. SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’96), Philadelphia, PA., May 1996.
Describes approach for exploiting annotations added to code to detect a wide class of errors. Focuses on memory management checks described in Section 5 of this manual.
[Evans00] David Evans. Annotation-Assisted Lightweight Static Checking. First International Workshop on Automated Program Analysis, Testing and Verification. February, 2000.
Short position paper describing research agenda behind Splint.
[Evans02] David Evans and David Larochelle. Improving Security Using Extensible Lightweight Static Analysis. IEEE Software, Jan/Feb 2002.
Most security attacks exploit instances of well-known classes of implementations flaws. This article describes how Splint can be used to detect common security vulnerabilities (including buffer overflows and format string vulnerabilities).
[Larochelle01] David Larochelle and David Evans. Statically Detecting Likely Buffer Overflow Vulnerabilities. 2001 USENIX Security Symposium, Washington, D. C., August 13-17, 2001.
Buffer overflow attacks may be today's single most important security threat. This paper describes how Splint can be used to detect likely vulnerabilities through an analysis of the program source code and presents experience using our approach to detect buffer overflow vulnerabilities in two security-sensitive programs.
[ISO99] International Standard ISO/IEC 9899. Programming languages – C. Second edition. December 1999.
International standard specification for C programming language. Approved by ANSI May 2000.
[KR88] Brian W. Kernighan and Dennis M. Ritchie. The C Programming Language, second edition. Prentice Hall, New Jersey, 1988.
Standard reference for ANSI C. If you haven’t heard of this one, you probably didn’t get this far (unless you started at the back).
[vdL94] Peter van der Linden. Expert C Programming: Deep C Secrets. SunSoft Press, Prentice Hall, New Jersey, 1994.
Filled with useful information on the darker corners of C, as well as lots of industry anecdotes and humor. Splint’s reserved name checking is loosely based on the list of reserved names in this book.
[GH93] John Guttag and James Horning with Stephen J. Garland, Kevin D. Jones, Andrés Modet, and Jeannette M. Wing. Larch: Languages and Tools for Formal Specification. Springer-Verlag, Texts and Monographs in Computer Science, 1993.
Overview of the Larch family of specification languages and related tools. Includes a chapter on LCL, the Larch C interface language, on which Splint is based.
[LG86] Barbara Liskov and John Guttag. Abstraction and Specification in Program Development, MIT Press, Cambridge, MA, 1986.
Describes a programming methodology using abstract types and specified interfaces. Much of the methodology upon which Splint is based comes from this book. Uses the CLU programming language.
[Liskov01] Barbara Liskov with John Guttag. Program Development in Java, Addison Wesley, 2001.
An updated version of [LG86] for the Java programming language.
[Tan95] Yang Meng Tan. Formal Specification Techniques for Engineering Modular C. Kluwer International Series in Software Engineering, Volume 1, Kluwer Academic Publishers, Boston, 1995.
Modified and updated version of MIT Ph D thesis, previously published as MIT/LCS/TR-619, 1994. Includes presentation of the semantics of LCL and a case study using LCL.
[Hat95] Les Hatton. Safer C: Developing Software for High-integrity and Safety-critical Systems. McGraw-Hill International Series in Software Engineering, 1995.
A broad work on all aspects of developing safety-critical software, focusing on the C language. Provides good justification for the use of C in safety-critical systems, and the necessity of tool-supported programming standards. Splint users will be interested to see how many of the errors listed as only being dynamically detectable can be detected statically by Splint.
[VM02] John Viega and Gary McGraw. Building Secure Software: How to Avoid Security Problems the Right Way. Addison-Wesley, 2002.
A comprehensive survey of techniques and principles for building secure programs.
See also [Evans02] and [Larochelle01].