Inexpensive Program Analysis

IPA
Inexpensive Program Analysis
at the University of Virginia
If you want a guarantee, buy a toaster.
Clint Eastwood (The Rookie, 1990)

Courses - Funding - Papers - People - Software - Talks

Research Summary
Despite considerable progress in program analysis tools, typical software development processes make little use of advanced analysis techniques, even when they are producing mission critical software. Our group is exploring analysis approaches that combine dynamic and static analysis techniques.
We co-organized the Workshop on Dynamic Analysis (25 May 2004, colocated with ICSE).
Software

Splint
Splint is a tool for statically checking C programs for security vulnerabilities and coding mistakes. With minimal effort, Splint can be used as a better lint. If additional effort is invested adding annotations to programs, Splint can perform stronger checking than can be done by any standard lint.
Perracotta
Perracotta is a dynamic analysis tool for automatically inferring temporal properties of a target program. It takes the program's execution traces as input and outputs a set of likely temporal properties. The properties can enhance program understanding, be used to aid program evolution, or be used as input properties for a model checker.

Courses

CS201J: Engineering Software, Fall 2003
CS201J: Engineering Software, Fall 2002
CS201J is an introductory software engineering (CS2) course focused on teaching students to produce dependable and secure software. It uses lightweight analysis tools (primarily ESC/Java) throughout the course.

Selected Papers
See http://www.cs.virginia.edu/evans/pubs/ for full publications list
Jinlin Yang, David Evans, Deepali Bhardwaj, Thirumalesh Bhat, Manuvir Das. Perracotta: Mining Temporal API Rules From Imperfect Traces. 28th International Conference in Software Engineering, Research Track, Shanghai, China, May 2006.
David Evans and Michael Peck. Inculcating Invariants in Introductory Courses. 28th International Conference in Software Engineering, Education Track, Shanghai, China, May 2006.
David Evans. Toasters, Seat Belts, and Inferring Program Properties . IFIP Working Conference on Verified Software: Theories, Tools, Experiments. Zürich, Switzerland. 10-13 October 2005. (PDF, 8 pages)
Jinlin Yang and David Evans. Automatically Inferring Temporal Properties for Program Evolution. Fifteenth IEEE International Symposium on Software Reliability Engineering (ISSRE 2004). Saint-Malo, France. 2-5 November 2004. (PDF, 12 pages)
Jinlin Yang and David Evans. Dynamically Inferring Temporal Properties. ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2004). 7-8 June 2004. (PDF, 6 pages)
Michael Peck. Improving the Usability of the ESC/Java Static Analysis Tool. University of Virginia Fourth Year Thesis. 25 March 2004. (PDF, 26 pages)
Joel Winstead and David Evans. Towards Differential Program Analysis. Workshop on Dynamic Analysis. 9 May 2003. (PDF, 4 pages)
David Evans and David Larochelle. Improving Security Using Extensible Lightweight Static Analysis. IEEE Software, Jan/Feb 2002. (PDF, 10 pages) (CiteSeer Page, 16 citations)
David Larochelle and David Evans. Statically Detecting Likely Buffer Overflow Vulnerabilities. USENIX Security Symposium 2001. [PDF] (CiteSeer Page, 25 citations)
David Evans. Static Detection of Dynamic Memory Errors. SIGPLAN Conference on Programming Language Design and Implementation (PLDI '96), May 1996. [PDF] (CiteSeer Page, 79 citations)
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. [PDF] (55 citations, CiteSeer Page)
See http://www.splint.org/pubs/ for more publications about Splint and LCLint. See http://www.cs.virginia.edu/evans/pubs/ for more papers by David Evans.

Talks

Automatically Inferring Temporal Properties for Program Evolution [PPT] (Jinlin Yang and David Evans). Conference talk at 15th IEEE International Symposium on Software Reliability Engineering (ISSRE 2004). 5 November 2004.
Dynamically Inferring Temporal Properties for Daisy [PPT] (Jinlin Yang). Technical talk at the Joint CAV/ISSTA Special Event on Specification, Verification, and Testing of Concurrent Software. July 14, 2004.
Dynamically Inferring Temporal Properties [PPT] (Jinlin Yang). Technical talk at ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2004). 7 June 2004.
Finding Security Vulnerabilities Before Evildoers Do [SXI (OpenOffice), PPT] (David Evans). Invited talk at Conferencia Internacional de Software Libre, Malaga, Spain, 20 February 2004.
Statically Detecting Likely Buffer Overflow Vulnerabilities (David Larochelle) [PPT] [PDF]. USENIX Security '01 for Statically Detecting Likely Buffer Overflow Vulnerabilities.
Extensible Lightweight Static Checking [PPT] [PDF] (David Evans). Short talk at University of Washington and Microsoft Research Summer Institute on Specifying and Checking Properties of Software, 14 August 2001.
Let's Stop Beating Dead Horses and Start Beating Trojan Horses [PPT] (David Evans). Short presentation in a debate on Proof-Carrying Code with Peter Lee at the Infosec Research Council, Malicious Code Study Group. San Antonio, 13 January 2000.
Systems for Safety and Dependability [PPT] (David Evans). Invited seminar at Reliable Software Technologies. Sterling, VA, 14 December 1999.

People

Project Leader: David Evans
Current PhD Students
    Jinlin Yang
    Joel Winstead
Current Undergraduate Students
    Ed Mitchell
Alumni
    David Larochelle (MCS 2001)
        MCS Project: Statically Detecting Likely Buffer Overflow Vulnerabilities
    Mike Peck (BS 2004) — graduate student at Johns Hopkins University
        Thesis: Improving the Usability of the ESC/Java Static Analysis Tool
    David Friedman (BS 2002) — graduate student at Johns Hopkins University
        Thesis: Using Splint to Detect Buffer Overflow Vulnerabilities in Sendmail
    Michael Lanouette (BS 2002)
        Thesis: Static Checking of Coding Standards
    Hien Phan (BS 2002)
        Thesis: Developing a Web Interface for the LCLint Static Checker

Other LCLint and Splint Contributors

Funding
Our research is partially supported by the National Science Foundation through

CPA: Automatic Inference and Effective Use of Temporal Properties (Award 0541123), 2006-2008.

Previously, we have been supported by these grants:

ITR: A Framework for Environment-Aware, Massively Distributed Computing (with Tarek Abdelzaher and David Brogan), 2001 - 2005.
CAREER: Programming the Swarm, 2000 - 2006. (PDF, PS, NSF Page)

CCLI: Teaching Software Engineering Using Lightweight Analysis, January 2002 - December 2003. (PDF, PS)

Previously, our work was funded by a grant from NASA and a USENIX Student Research Grant.