Photo Scott McPeak
565 Soda Hall
510-642-9542
smcpeak {at} cs {dot} berkeley {dot} edu
PGP key
Resume (or in PDF)
Research Statement (or in PDF)
Campanile

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/Java distribution.

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.

Elkhound and Elsa

Elkhound 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.

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).

Miscellaneous

"What is latex?", in under five minutes.

I wrote up a solution for how to do secure, remote CVS access with a shared guest account but accurate per-user CVS commit info.

I recently bought a Samsung ML-1430 laser printer and managed to get it working under Linux; here's how.

A short note on Debugging Memory Errors in C/C++

Gnus tutorial

Autodependencies with GNU make

Module dependency scanner

Linux on a Compaq Presario 1830
(Penguin anim ruthlessly stolen from here)

Melee: a cross between Warcraft, RoboSport, and a role-playing game.

Feudal C stuff

I've put together some stuff on hacking emacs.

A long time ago I participated in some investigation of 2-3 trees.