David Lie
Associate Professor
Department of Electrical & Computer Engineering
Sanford Flemming 2001C
10 King's College Road
Toronto, ON M5S 3G4
lie@eecg.toronto.edu (PGP key)
Phone: (416) 946-0251
Fax: (416) 971-2326
Admin: Beverly Chu, (416) 946-8094

• Home
• Publications & Talks
• Students
• Sponsors
• Directions

Publications

Refereed Conference and Workshop Publications

• Lionel Litty, H. Andrés Lagar-Cavilla and David Lie.Computer Meteorology: Monitoring Compute Clouds. In Proceedings of the 12th Workshop on Hot Topics in Operating Systems (HotOS 2009). May 2009. (This position paper provides a taxonomy of virtual machine introspection techniques for monitoring cloud infrastructures and proposes a new technique, architectural introspection, which provides better properties for cloud monitoring.)
• Thomas 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 buffer programming idioms. A full length technical report can be found here.)
• Thomas 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 to verify the absence of buffer overflows.)
• 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. This system makes no assumptions about the OS kernel, relying instead on only binary the format specification and processor hardware.)
• Thomas 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.)
• Kelvin Ku, Thomas 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 buffer overflow 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 strength 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 for a technique that allows 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 uses a hypervisor to enable applications to use a commodity operating system without having to trust it.)
• 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 introduces XOMOS, an operating system for the XOM processor architecture, which allows applications to execute without having to trust the OS.)
• 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 processor 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 checking 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 presents the XOM processor architecture, which allows applications to hide secrets from a malicious adversary who controls the OS and has physical access to the computer hardware.)

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. In the IEEE Transactions on Computing. Vol 53, No. 12., Pages 1557-1568. December 2004. (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 description of the XOM processor architecture)
• David Lie. Architectural Support for Copy and Tamper-Resistant Software, Ph.D Thesis, 2003. (Good bed time reading)
• Thomas Hart, Kelvin Ku, David Lie, Marsha Chechik, and Arie Gurfinkel. Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates. Technical Report CSRG-581, University of Toronto. September 2008

back to top - © 2009 David Lie - all rights reserved. Last modified: 2009-07-31