Scott McPeak (original) (raw)

| | | | --------------------------------------------------------------------------------------------------------- |

I am a graduate student in Computer Science at UC Berkeley. My advisor is George Necula. My research focus is on program verification with formal methods, in particular verifying pointer-intensive programs written in unsafe languages like C. I also dabble in parsing and run-time safety checking, and am interested in software engineering and security.

Verifier

I am working on building a program verifier for C programs. An initial release is here:<verifier-2005.07.05.tar.gz>. To build and test it, say:

./configure && make && cd verifier && ./regrtest

This release has not had much portability testing yet. Some tests require the Simplify theorem prover, which can be obtained as part of the ESC/Javadistribution.

My work is closely related to that of Greg Nelson; since his thesis was nontrivial to find, I've scanned and posted it (with permission):Greg Nelson's PhD thesis.

CCured

CCured("see-cured") is a source-to-source translator for C that inserts run-time checks for memory safety. The resulting program will either run normally, or it will abort due to a memory safety violation (such as a buffer overrun). We have used it to create memory-safe versions of a number of popular network server programs, such as ftpd and sshd. We therefore believe these servers to be immune to (e.g.) stack smashing attacks.

CCured: Type-Safe Retrofitting of Legacy Software
George C. Necula, Jeremy Condit, Matthew Harren, Scott McPeak, Westley Weimer
In ACM Transactions on Programming Languages and Systems (TOPLAS), to appear, 2004
CCured in the Real World
Jeremy Condit, Mathew Harren, Scott McPeak, George C. Necula, Westley Weimer
In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI03), June 2003.
CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs
George C. Necula, Scott McPeak, S. P. Rahul, Westley Weimer.
In Proceedings of Conference on Compiler Construction (CC02), March 2002.
CCured: Type-Safe Retrofitting of Legacy Code
George C. Necula, Scott McPeak, Westley Weimer.
In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (POPL02), January 2002.

Elkhound and Elsa

	Elkhound is a parser generator utilizing the Generalzed LR (GLR) parsing algorithm. It is an especially fast implementation, being competitive with LALR(1) implementations such as Bison for deterministic input fragments.

Elsa is a C++ parser written using Elkhound and taking advantage of its support for ambiguous grammars to handle tricky aspects of C++ syntax.

Elkhound: A Fast, Practical GLR Parser Generator
Scott McPeak, George C. Necula.
In Proceedings of Conference on Compiler Constructor (CC04), April 2004.
An expanded technical report isUCB/CSSD-2-1214.

SafeTP

SafeTP ("safe-tee-pee") is an FTP proxy client and server that encrypts the communications between an ordinary, unmodified FTP client/server pair. The result is a secure communication session with legacy software. SafeTP is similar to a virtual private network, except it operates at the application layer instead of the network layer (so it is easier to setup and tear down, but application-specific).