Publications
Refereed Conference and Workshop Publications
- Boem Heyn Kim, Wei Huang and David Lie. Unity: Secure and Durable Personal Cloud Storage. In Proceedings of the ACM Cloud Computing Security Workshop (CCSW 2012). October 2012. (Unity is a new secure personal storage system that protects the confidentiality, integrity and availability of the user's data even if the cloud provider is malicious. To acheive this, Unity stores user data only on the user's devices and uses the cloud provider only as a highly available and reliable coordination server.)
- Kathy Wain Yee Au, Yi Fan Zhou, Zhen Huang and David Lie. PScout: Analyzing the Android Permission Specification. In Proceedings of the 19th ACM Conference on Computer and Communications Security (CCS 2012). Pages 217-228. October 2012. [Download Source Code and Permission Maps] (A great paper that tries to answer questions about the right granularity, the right trade-offs and the state of the Android permission system. It also shows off a static analysis tool called PScout, which we built to extract permission specifications from Android.)
- Afshar Ganjali and David Lie. Auditing Cloud Administrators Using Information Flow Tracking . In Proceedings of the The Seventh ACM Workshop on Scalable Trusted Computing (STC 2012). October 2012. (H-One is a proposal that uses information flow to provide complete, efficient and privacy preserving auditing logs for IaaS cloud services.)
- Mohammad Mannan, Beom Heyn Kim, Afshar Ganjali and David Lie. Unicorn: Two-Factor Attestation for Data Security. In Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS 2011). Pages 17-28. October 2011. (A neat idea on how to implement defense in depth for trusted computing by having two devices independently protect your data.)
- Kathy Wain Yee Au, Yi Fan Zhou, Zhen Huang, Phillipa Gill and David Lie. Short Paper: A Look at SmartPhone Permission Models. In Proceedings of the 1st ACM CCS Workshop on Security and Privacy in Smartphones and Mobile Devices (SPSM 2011). Pages 63-67. October 2011. A short position paper describing an approach we are taking to produce a tool to prevent overdeclaration of permissions in Android. Also of use is a survey and taxonomy of the various permission systems in popular smartphone operating systems.
- Lionel Litty and David Lie. Patch Auditing in Infrastructure as a Service Clouds. In Proceedings of the 2011 ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments (VEE 2011). Pages 145-156. March 2011. (This paper builds on our Patagonix system to detect out of date executables by extendin monitoring to non-binary code and to enable checking of resumed VMs.)
- Mohammed Mannan, David Barrera, Carson Brown, David Lie, Paul van Oorschot. Mercury: Recovering Forgotten Passwords Using Personal Devices (Pre-proceedings). In Proceedings of Financial Cryptography and Data Security 2011 (FC'11). February 2011. (In this paper, we propose Mercury, a system for easily and security recovering forgotten passwords with use of a smart phone.)
- David Lie and Lionel Litty. Using Hypervisors to Secure Commodity Operating Systems. In the Fifth Annual Workshop on Scalable Trusted Computing (Invited Paper). October 2010. (This paper summarizes recent work in using hypervisor to secure commodity systems. We also provide some of the insights we have gained through doing our own work in the area.)
- Phillipa Gill, Yashar Ganjali, Bernard Wong and David Lie. Dude, Where's That IP? Circumventing Measurement-based IP Geolocation. In Proceedings of the 19th USENIX Security Symposium. August 2010. (An exploration of whether state of the art geolocation techniques can stand up to a malicious adversary that tries to subvert network measurements. Turns current geolocation methods are susceptible to attack, and that the more sophisticated and precise geolocation methods are actually more vulnerable!)
- Lee Chew and David Lie. Kivati: Fast Detection and Prevention of Atomicity Violations. In Proceedings of the 2010 EuroSys Conference (EuroSys 2010), Pages 307-320. April 2010. (Kivati uses hardware watchpoints, to aggressively find and remove potential atomicity violations. While hardware watchpoints do not impose much performance overhead, they do require traps into the kernel to turn on and off, so Kivati uses a number of clever tricks to minimize trips into the kernel while still maintaining consistency among watchpoints on different cores.)
- 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
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]
