I am Dave King, a PhD candidate at Penn State in Computer Science and Engineering. My research interests are security-typed languages, automatic security generation and verification, and software engineering. My advisor is Trent Jaeger. I have been a member of the Systems and Internet Infrastructure Security Laboratory since Fall 2007. My planned graduation date is Spring 2009.

My main research focus is on trusted programs; i.e. programs that are trusted by the system to enforce system-wide security goals such as maintaining secrecy or integrity of data. A developing way to build trusted programs is by using security-typed languages, which provide compilers to verify the information-flow security (secret information is not leaked to public) of programs. Some example security-typed languages are Jif, Flow Caml, and SELinks. However, as most programs are not information-flow secure "out of the box", we are working to improve these tools to ease the process of adding information-flow guarantees to real-world programs. More information about this can be found on my research page.

I received dual degrees in both Computer Science and Mathematics from the University of Illinois at Urbana-Champaign. During my first three years at Penn State, I investigated polymorphic references in functional languages with John Hannan. I have also been the recipient of a Lockheed Martin Software Engineering Fellowship and the Penn State CSE Graduate Student Teaching Assistant Award.

I have created a number of tools to help programmers use the security-typed language Jif. Boniface Hicks and I developed Jifclipse, an IDE for Jif using Eclipse. I have also released blame-enabled Jif, a modification of the Jif compiler to provide error traces for failed constraints. JLift extends the Jif compiler with a whole-program analysis for (most) Java programs, and siggen can be used to generate signatures (corresponding to external library calls) for Jif programs.

Contact Information:

News:

September 4, 2008: Our paper, "Implicit Flows: Can't Live With 'Em, Can't Live Without 'Em" (with Boniface Hicks, Trent Jaeger, and Michael Hicks) has been accepted for publication and will appear at the Fourth International Conference on Information System Security (ICISS 2008).

July 14, 2008: I will be presenting a poster, "Retrofitting Programs for Information-Flow Security", at the 2008 USENIX Security Symposium in San Jose, CA.

July 3, 2008: I have been awarded a travel grant to attend the 2008 USENIX Security Symposium in San Jose, CA.

May 28, 2008: Our paper, "Effective Blame for Information-Flow Violations" (with Trent Jaeger, Somesh Jha, and Sanjit A. Seshia) has been accepted for publication and will appear at the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2008).

April 5, 2008: Our paper, "Verifying the Compliance of Trusted Programs" (with Sandra Reuda and Trent Jaeger) has been accepted for publication and will appear at the 17th USENIX Security Symposium (USENIX 2008).

Publications:

A complete list of my publications and technical reports can be found here.

Software:

Jifclipse: Jif IDE built in Eclipse.

JLift: an extension of the Jif compiler for whole-program analysis.

siggen: Automatically generate Jif signatures for your Java/Jif code.

Blame-Enabled Jif: Error traces for your Jif programs. (implementation of FSE 2008 results)

A patch to get xinetd to play nicely with SELinux and labeled IPSec: processes are started at the context of the requestor, rather than the context of xinetd.

Teaching:

Teaching Assistant: CMPSC 101 (Business Computing Applications). Spring 2004.

Teaching Assistant: CSE 120 (Data Structures). Fall 2004 - Spring 2005.

Instructor: CSE 271 (Digital Logic). Fall 2006.

Instructor: CMPSC 101 (Introduction to Programming with Visual Basic). Spring 2007

Personal:

Personal Information

Links