Talks and Publications

Refereed Conference and Workshop Publications

Thomas E. Hart, Kelvin Ku, David Lie, Marsha Chechik, and Arie Gurfinkel. Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates.   In Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008).   September, 2008.  (This paper describes Proof Templates, a technique for providing an abstracted proof, which a CEGAR model checker can use to prove correctness of code that uses common programming idioms for manipulating buffers. A full length technical report can be found here.)

Thomas E. Hart, Kelvin Ku, David Lie, Marsha Chechik, and Arie Gurfinkel. PtYasm: Software Model Checking with Proof Templates.   In Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008).   September, 2008.  (This paper describes PtYasm, our tool for inserting proof< templates into Yasm, a software model checker.)

Thomas E. Hart, Marsha Chechik, and David Lie. Security Benchmarking using Partial Verification.   In Proceedings of the 3rd Workshop on Hot Topics in Security (HotSec 2008).   July, 2008.  (This paper proposes a novel use for formal verification tools -- as a mechanism for measuring security strength of software.)

Lionel Litty, H. Andrés Lagar-Cavilla and David Lie. Hypervisor Support for Identifying Covertly Executing Binaries  In the 17th Usenix Security Symposium. Pages 243-258.   July, 2008.  (A hypervisor based system that neutralizes the ability of rootkits to hide executing binaries from< the administrator. This system makes no assumptions about the OS kernel, relying instead on binary format specifications and processor hardware.)

Kelvin Ku, Thomas E. Hart, Marsha Chechik, and David Lie. A Buffer Overflow Benchmark for Software Model Checkers.  In Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007).  November, 2007.  (This paper describes a realistic suite of benchmarks for SMC's based on vulnerabilities found in various databases such as CVE.)

David Lie and M. Satyanarayanan. Quantifying the Strength of Security Systems.  In Proceedings of the 2nd Workshop on Hot Topics in Security (HotSec 2007).  August, 2007.  (Fun paper on a challenge-based scheme for quantitatively measuring the strenght of security components.)

Jesse Pool, Ian Sin and David Lie. Relaxed Determinism: Making Redundant Execution on Multiprocessors Practical.  In Proceedings of the 11th Workshop on Hot Topics in Operating Systems (HotOS 2007).  Pages 25-30. May, 2007.  (Description and preliminary results of a technique to allow redundant execution to work on multi-core processors by relaxing the determinism requirements between replicas)

Richard Ta-Min, Lionel Litty and David Lie. Splitting Interfaces: Making Trust Between Applications and Operating Systems Configurable.  In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2006).  Pages 279-292. November, 2006.  (This paper presents a system that allows applications to use commodity operating systems without having to trust them in their entirety)

Lionel Litty and David Lie. Manitou: A Layer-Below Approach to Fighting Malware.  In Proceedings of the Workshop on Architectural and System Support for Improving Software Dependability (ASID), held in conjunction with ASPLOS 2006. Pages 6-11.  October, 2006.  (This paper introduces some ideas on using hardware support to combat malware.)

Kurniadi Asrigo, Lionel Litty and David Lie.  Using VMM-Based Sensors to Monitor Honeypots.  In Proceedings of the 2nd International Conference on Virtual Execution Environments (VEE 2006).   Pages 13-23.  June, 2006. (This paper talks about our experiences with using virtual machine monitors to collect information from honeypots.)

David Lie,  Chandramohan Thekkath and Mark Horowitz.  Implementing an Untrusted Operating System on Trusted Hardware.  In Proceedings of the 19th ACM Symposium on Operating Systems Principles (SOSP 2003).  October, 2003. Best Paper Award! (This paper discusses how to write an operating system for XOM.)

David Lie, John Mitchell, Chandramohan Thekkath and Mark Horowitz.   Specifying and Verifying Hardware for Tamper-Resistant Software.   In Proceedings of the 2003 IEEE Symposium on Security and Privacy.  May, 2003. (This paper discusses a formal model and  verification of the XOM architecture.)

David Lie, Andy Chou, Dawson Engler and David Dill.  A Simple Method for Extracting Models from Protocol Code.  In Proceedings of the 28th International Symposium on Computer Architecture (ISCA 2001).  July, 2001. (This paper discusses compiler-aided formal verification techniques for cache coherence protocols)

Deqing Chen, Alan Messer, Philippe Bernadat, Guangrui Fu, Zoran Dimitrijevic, David Lie, Durga Mannaru, Alma Riska, and Dejan Milojicic.  JVM Susceptibility to Memory Errors.  In Proceedings of the Java Machine Research and Technology Symposium (JVM 2001).  April, 2001. (A paper I did while I was an intern at HP Labs.  This paper is on reliability and recoverability of JVM's in the face of soft errors in memories.)

David Lie, Chandramohan Thekkath, Mark Mitchell, Patrick Lincoln, Dan Boneh, John Mitchell, and Mark Horowitz.  Architectural Support for Copy and Tamper Resistant Software .  In Proceedings of the 9th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-IX).  November, 2000. (This paper discusses the XOM architecture in detail)

Refereed Journal Publications

Alan Messer, Phillippe Bernadat, Guangrui Fu, Deqing Chen, Zoran Dimitrijevic, David Lie, Durga Devi Mannaru, Alma Riska and Dejan Milojicic. Susceptibility of Commodity Systems and Software to Memory Soft Errors.  To appear in the IEEE Transactions on Computing. (Joint work done with the fault tolerance group at HP Labs)

Unrefereed Publications

Dan Boneh, David Lie, Patrick Lincoln, John Mitchell, Mark Mitchell. Hardware Support for Tamper-Resistant and Copy-Resistant Software,  Technical Report CS-TN-00-97, Stanford University Computer Science, 2000. (A preliminary draft of the XOM architecture)

David Lie. Architectural Support for Copy and Tamper-Resistant Software, Ph.D Thesis, 2003. (Good bed time reading)

Selected Talks

Splitting Interfaces: Making Trust between Applications and Operating Systems Configurable.  OSDI 2006. (pdf)

Implementing an Untrusted Operating System on Trusted Hardware.  SOSP 2003. (html, pdf, ppt)

Architectural Support for Copy and Tamper Resistant Software.  2003. (html, pdf, ppt)

Specifying and Verifying Hardware for Tamper-Resistant Software.  Oakland 2003. (html, pdf, ppt)

A Simple Method for Extracting Models from Protocol Code.  ISCA 2001. (html, pdf, ppt)

Architectural Support for Copy and Tamper Resistant Software.  ASPLOS 2000. (html, pdf, ppt)

This page was last updated on 05/12/08.