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.
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 && ./regrtestThis 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 ("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 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 ("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).
"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++
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.