EDBT 2026 Demo / reviewers in the wild / expert
David Lie
dblp:l/DavidLie
· DBLP profile ↗
50ranked-venue papers
6as first author
19since 2021 · last 2026
0000-0002-2000-6827ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Security and privacy · 30 · 2 first-author · 14 since 2021Software engineering, systems software and programming languages · 15 · 4 first-author · 3 since 2021Systems, architecture and hardware · 9 · 2 first-author · 3 since 2021Artificial intelligence and machine learning · 1 · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Breaking the Illusion: Automated Reasoning of GDPR Consent Violations
Ying Li 0095, Wenjun Qiu, Faysal Hossain Shezan, Kunlin Cai, Michelangelo van Dam, Lisa M. Austin, David Lie, Yuan Tian 0001 |
SP | 7 |
| 2026 | GPUBreach: Privilege Escalation Attacks on GPUs Using RowhammerabstractNVIDIA GPUs with GDDR memories have been shown susceptible to Rowhammer-based bit-flips, similar to CPUs. However, Rowhammer exploits on GPUs have been limited to injecting untargeted bit-flips in victim data like weights of machine learning models, to degrade model accuracy, unlike CPU exploits shown capable of privilege escalation. In this paper, we demonstrate that GPU Rowhammer exploits can be as potent as CPU Rowhammer attacks. By exploiting the GPU page table management to identify when and where new page tables are allocated, we enable an unprivileged user CUDA kernel of one process to use RowHammer bit-flips to gain access to the GPU memory of other processes or co-tenants via targeted tampering of such page-tables resident on the GPU memory. Using this newly found primitive, we demonstrate the first GPU-side privilege escalation attacks, leaking secret data such as cryptographic keys from cuPQC libraries, and even tampering with the model's GPU assembly code to degrade models more stealthily than previous attacks. We further demonstrate that GPU-side privilege escalation can lead to CPU-side privilege escalation, defeating the protections provided by the IOMMU, enabling a malicious user-level program with GPU access to gain root shell and system-wide control, even in a non-multi-tenant setting. Chris S. Lin, Yuqin Yan, Guozhen Ding, Joyce Qu, Joseph Zhu, David Lie, Gururaj Saileshwar |
SP | 6 |
| 2025 | PSan: Towards Hybrid Metadata Scheme for Efficient Pointer CheckingabstractMemory safety remains at risk for programs written in unsafe languages like C. Pointer-checking schemes provide memory safety protection by attaching metadata for each pointer and checking them before dereference. Previously, sanitizers maintaining large per-pointer metadata (e.g., pointer bounds) were stuck with shadow memory for metadata storage, which incurs high overhead. Although fat pointers (i.e., instrumenting programs to inline metadata with pointers) incur less overhead, they introduce incompatibility issues to the instrumented programs, and are thus not considered by software-only sanitizers yet. In this paper, we push the status quo on adopting fat pointers for software-only pointer checking schemes and evaluate the benefit of this approach. We present PSan (short for “Pointer Sanitizer”), the first memory safety sanitizer that enables both inline and shadow memory metadata simultaneously in the same program. To reduce the overhead from shadow memory, PSan uses whole-program analysis and transformation to inline the metadata whenever possible, while using shadow memory only when necessary for compatibility. PSan-instrumented programs preserve binary compatibility with third-party uninstrumented code. In addition, PSan's framework decouples metadata management from checking, facilitating its augmentation with additional checkers. We evaluate the benefit of metadata inlining and observe that PSan's hybrid scheme reduces the runtime and memory overhead. Specifically, PSan incurs 40% lower overhead than popular memory checker SoftBoundCETS, which utilizes only shadow memory. Predictably, using inline metadata has a higher performance improvement when it can be applied to the majority of pointers in the program. Shengjie Xu 0001, Eric Liu 0001, Wei Huang 0027, Ilya Grishchenko, David Lie |
ACSAC | 5 |
| 2025 | EvoCrawl: Exploring Web Application Code and State using Evolutionary Search
Akshay Kawlay, Eric Liu 0001, David Lie |
NDSS | 4 |
| 2025 | Duumviri: Detecting Trackers and Mixed Trackers with a Breakage Detector
He Shuang, Lianying Zhao, David Lie |
NDSS | 3 |
| 2025 | Relocate-Vote: Using Sparsity Information to Exploit Ciphertext Side-Channels
Yuqin Yan, Wei Huang 0027, Ilya Grishchenko, Gururaj Saileshwar, Aastha Mehta, David Lie |
USENIX Security Symposium | 6 |
| 2024 | Exploring Strategies for Guiding Symbolic Analysis with Machine Learning PredictionabstractTo improve the scalability of symbolic analysis tools, one observation is that analysis resources are wasted on analyzing unsatisfiable paths, which are not possible in reality. While existing works attempt to predict the satisfiability of a program path without spending resources to analyze it, the performance of these predictor models are far from perfect. In this work, we attempt to understand how model predictions, even if imperfect, can be most effectively used to reduce the time required to analyze satisfiable paths. This work studies the sometimes complex interactions between model performance, analysis domain properties such as the distribution of path analysis costs and distribution of satisfiable paths, the design of symbolic analysis tools being used, and the algorithm used to prioritize and select paths for analysis. Using a novel simulation methodology, we study this problem and find that a number of factors can have as large an effect on symbolic analysis performance as improved predictors. Finally, we conclude with a couple of observations about how to best integrate machine learning prediction into symbolic analysis. David Lie, Nicolas Papernot |
SANER | 2 |
| 2023 | vWitness: Certifying Web Page Interactions with Computer VisionabstractWeb servers service client requests, some of which might cause the web server to perform security-sensitive operations (e.g. money transfer, voting). An attacker may thus forge or maliciously manipulate such requests by compromising a web client. Unfortunately, a web server has no way of knowing whether the client from which it receives a request has been compromised or not-current “best practice” defenses such as user authentication or network encryption cannot aid a server as they all assume web client integrity. To address this shortcoming, we propose vWitness, which “witnesses” the interactions of a user with a web page and certifies whether they match a specification provided by the web server, enabling the web server to know that the web request is user-intended. The main challenge that vWitness overcomes is that even benign clients introduce unpredictable variations in the way they render web pages. vWitness differentiates between these benign variations and malicious manipulation using computer vision, allowing it to certify to the web server that 1) the web page user interface is properly displayed 2) observed user interactions are used to construct the web request. Our vWitness prototype achieves compatibility with modern web pages, is resilient to adversarial example attacks and is accurate and performant-vWitness achieves 99.97% accuracy and adds 197ms of overhead to the entire interaction session in the average case. He Shuang, Lianying Zhao, David Lie |
DSN | 3 |
| 2023 | FLUX: Finding Bugs with LLVM IR Based Unit Test CrossoversabstractOptimizing compilers are as ubiquitous as they are crucial to software development. However, bugs in compilers are not uncommon. Among the most serious are bugs in compiler optimizations, which can cause unexpected behavior in compiled binaries. Existing approaches for detecting such bugs have focused on end-to-end compiler fuzzing, which limits their ability for targeted exploration of a compiler's optimizations. This paper proposes FLUX (Finding bugs with LLVM IR based Unit test cross(X)overs), a fuzzer that is designed to generate test cases that stress compiler optimizations. Previous compiler fuzzers are overly constrained by having to construct well-formed inputs. FLUX sidesteps this constraint by using human-written unit test suites as a starting point, and then selecting random combinations of them to generate new tests. We hypothesize that tests generated this way will be able to explore new execution paths through compiler optimizations and find new bugs. Our evaluation of FLUX on LLVM indicates that it is able to increase path coverage over the baseline LLVM unit test suite and explores more edge coverage than previous work. Further, we demonstrate FLUX's ability to generate miscompiled and crash-producing IR on LLVM's optimizations. After a month of fuzzing, FLUX found 28 unique bugs in LLVM's active development branch. We have reported 11 of these bugs which led to 6 of them being patched by LLVM developers. 22 of these are crashes that are triggered by well-formed input programs, and 6 of these are miscompilation bugs that silently produced incorrect code. Eric Liu 0001, Shengjie Xu 0001, David Lie |
ASE | 3 |
| 2023 | MIFP: Selective Fat-Pointer Bounds Compression for Accurate Bounds CheckingabstractBounds compression for fat pointers can reduce the memory and performance overhead of maintaining pointer bounds and is necessary for efficient hardware implementation. However, compression can introduce inaccuracy to the bounds, making certain out-of-bounds accesses undetectable. Although the security threat can be mitigated by padding the objects, no known mitigations can detect these out-of-bounds accesses deterministically. Shengjie Xu 0001, Eric Liu 0001, Wei Huang 0027, David Lie |
RAID | 4 |
| 2023 | Calpric: Inclusive and Fine-grain Labeling of Privacy Policies with Crowdsourcing and Active Learning
Wenjun Qiu, David Lie, Lisa M. Austin |
USENIX Security Symposium | 2 |
| 2022 | Driving Execution of Target Paths in Android Applications with (a) CARabstractDynamic program analysis is commonly used to vet Android applications. One approach is targeted execution, in which interesting or suspicious code is specifically targeted and analyzed dynamically. However, faithful execution to just the paths that reach these targets can be difficult due to the dependencies they have on other parts of the application. Prior works that handle dependencies must favor either soundness or completeness to the detriment of the other. Techniques that rely on precise dependency tracking ultimately result in lower coverage of targets due to overhead. Meanwhile, other techniques that aim for completeness by ignoring or bypassing dependencies lead to unsound execution and false positives. In this paper, we treat dependencies through the lens of a path context, which represents the program state expected by the path as it is executing. We propose an approach that provides better completeness and low false positives using Context Approximation and Refinement (CAR), which combines static constraint analysis and dynamic error recovery to infer a context based on the desired path flow and refine it during execution. We show that the integration of CAR with targeted execution can reach 3.1x more target locations in popular Android applications than the existing state of the art while having a false detection rate of 9%, enabling more complete analysis and detection of security-sensitive behaviors. Michelle Y. Wong, David Lie |
AsiaCCS | 2 |
| 2022 | In Differential Privacy, There is Truth: on Vote-Histogram Leakage in Ensemble Private LearningabstractWhen learning from sensitive data, care must be taken to ensure that training algorithms address privacy concerns. The canonical Private Aggregation of Teacher Ensembles, or PATE, computes output labels by aggregating the predictions of a (possibly distributed) collection of teacher models via a voting mechanism. The mechanism adds noise to attain a differential privacy guarantee with respect to the teachers' training data. In this work, we observe that this use of noise, which makes PATE predictions stochastic, enables new forms of leakage of sensitive information. For a given input, our adversary exploits this stochasticity to extract high-fidelity histograms of the votes submitted by the underlying teachers. From these histograms, the adversary can learn sensitive attributes of the input such as race, gender, or age. Although this attack does not directly violate the differential privacy guarantee, it clearly violates privacy norms and expectations, and would not be possible $\textit{at all}$ without the noise inserted to obtain differential privacy. In fact, counter-intuitively, the attack $\textbf{becomes easier as we add more noise}$ to provide stronger differential privacy. We hope this encourages future work to consider privacy holistically rather than treat differential privacy as a panacea. Roei Schuster, Ilia Shumailov, David Lie, Nicolas Papernot |
NeurIPS | 4 |
| 2022 | Modulo: Finding Convergence Failure Bugs in Distributed Systems with Divergence Resync Models
Beom Heyn Kim, Taesoo Kim, David Lie |
USENIX ATC | 3 |
| 2021 | In-fat pointer: hardware-assisted tagged-pointer spatial memory safety defense with subobject granularity protectionabstractProgramming languages like C and C++ are not memory-safe because they provide programmers with low-level pointer manipulation primitives. The incorrect use of these primitives can result in bugs and security vulnerabilities: for example, spatial memory safety errors can be caused by dereferencing pointers outside the legitimate address range belonging to the corresponding object. While a range of schemes to provide protection against these vulnerabilities have been proposed, they all suffer from the lack of one or more of low performance overhead, compatibility with legacy code, or comprehensive protection for all objects and subobjects. Shengjie Xu 0001, Wei Huang 0027, David Lie |
ASPLOS | 3 |
| 2021 | Aion Attacks: Manipulating Software Timers in Trusted Execution Environment
Wei Huang 0027, Shengjie Xu 0001, Yueqiang Cheng, David Lie |
DIMVA | 4 |
| 2021 | Emilia: Catching Iago in Legacy Code
Rongzhen Cui, Lianying Zhao, David Lie |
NDSS | 3 |
| 2021 | Machine UnlearningabstractOnce users have shared their data online, it is generally difficult for them to revoke access and ask for the data to be deleted. Machine learning (ML) exacerbates this problem because any model trained with said data may have memorized it, putting users at risk of a successful privacy attack exposing their information. Yet, having models unlearn is notoriously difficult.We introduce SISA training, a framework that expedites the unlearning process by strategically limiting the influence of a data point in the training procedure. While our framework is applicable to any learning algorithm, it is designed to achieve the largest improvements for stateful algorithms like stochastic gradient descent for deep neural networks. SISA training reduces the computational overhead associated with unlearning, even in the worst-case setting where unlearning requests are made uniformly across the training set. In some cases, the service provider may have a prior on the distribution of unlearning requests that will be issued by users. We may take this prior into account to partition and order data accordingly, and further decrease overhead from unlearning.Our evaluation spans several datasets from different domains, with corresponding motivations for unlearning. Under no distributional assumptions, for simple learning tasks, we observe that SISA training improves time to unlearn points from the Purchase dataset by 4.63×, and 2.45× for the SVHN dataset, over retraining from scratch. SISA training also provides a speed-up of 1.36× in retraining for complex learning tasks such as ImageNet classification; aided by transfer learning, this results in a small degradation in accuracy. Our work contributes to practical data governance in machine unlearning. Lucas Bourtoule, Varun Chandrasekaran, Christopher A. Choquette-Choo, Hengrui Jia 0001, Adelin Travers, Baiwu Zhang, David Lie, Nicolas Papernot |
SP | 7 |
| 2021 | A Large Scale Study of User Behavior, Expectations and Engagement with Android Permissions
Weicheng Cao, Chunqiu Xia, Sai Teja Peddinti, David Lie, Nina Taft, Lisa M. Austin |
USENIX Security Symposium | 4 |
| 2020 | Ex-vivo dynamic analysis framework for Android device driversabstractThe ability to execute and analyze code makes many security tasks such as exploit development, reverse engineering, and vulnerability detection much easier. However, on embedded devices such as Android smartphones, executing code in-vivo, on the device, for analysis is limited by the need to acquire such devices, the speed of the device, and in some cases the need to flash custom code onto the devices. The other option is to execute the code ex-vivo, off the device, but this approach either requires porting or complex hardware emulation. In this paper, we take advantage of the observation that many execution paths in drivers are only superficially dependent on both the hardware and kernel on which the driver executes, to create an ex-vivo dynamic driver analysis framework for Android devices that requires neither porting nor emulation. We achieve this by developing a generic evasion framework that enables driver initialization by evading hardware and kernel dependencies instead of precisely emulating them, and then developing a novel Ex-vivo AnalySIs framEwoRk (EASIER) that enables off-device analysis with the initialized driver state. Compared to on-device analysis, our approach enables the use of userspace tools and scales with the number of available commodity CPU's, not the number of smartphones. We demonstrate the usefulness of our framework by targeting privilege escalation vulnerabilities in system call handlers in platform device drivers. We find it can load 48/62 (77%) drivers from three different Android kernels: MSM, Xiaomi, and Huawei. We then confirm that it is able to reach and detect 21 known vulnerabilities. Finally, we have discovered 12 new bugs which we have reported and confirmed. Ivan Pustogarov, David Lie |
SP | 3 |
| 2019 | Using Safety Properties to Generate Vulnerability PatchesabstractSecurity vulnerabilities are among the most critical software defects in existence. When identified, programmers aim to produce patches that prevent the vulnerability as quickly as possible, motivating the need for automatic program repair (APR) methods to generate patches automatically. Unfortunately, most current APR methods fall short because they approximate the properties necessary to prevent the vulnerability using examples. Approximations result in patches that either do not fix the vulnerability comprehensively, or may even introduce new bugs. Instead, we propose property-based APR, which uses human-specified, program-independent and vulnerability-specific safety properties to derive source code patches for security vulnerabilities. Unlike properties that are approximated by observing the execution of test cases, such safety properties are precise and complete. The primary challenge lies in mapping such safety properties into source code patches that can be instantiated into an existing program. To address these challenges, we propose Senx, which, given a set of safety properties and a single input that triggers the vulnerability, detects the safety property violated by the vulnerability input and generates a corresponding patch that enforces the safety property and thus, removes the vulnerability. Senx solves several challenges with property-based APR: it identifies the program expressions and variables that must be evaluated to check safety properties and identifies the program scopes where they can be evaluated, it generates new code to selectively compute the values it needs if calling existing program code would cause unwanted side effects, and it uses a novel access range analysis technique to avoid placing patches inside loops where it could incur performance overhead. Our evaluation shows that the patches generated by Senx successfully fix 32 of 42 real-world vulnerabilities from 11 applications including various tools or libraries for manipulating graphics/media files, a programming language interpreter, a relational database engine, a collection of programming tools for creating and managing binary programs, and a collection of basic file, shell, and text manipulation tools. Zhen Huang 0002, David Lie, Gang Tan, Trent Jaeger |
IEEE Symposium on Security and Privacy | 2 |
| 2018 | Tackling runtime-based obfuscation in Android with TIRO
Michelle Y. Wong, David Lie |
USENIX Security Symposium | 2 |
| 2017 | Consistency Oracles: Towards an Interactive and Flexible Consistency Model SpecificationabstractMany modern distributed storage systems emphasize availability and partition tolerance over consistency, leading to many systems that provide weak data consistency. However, weak data consistency is difficult for both system designers and users to reason about. Formal specifications offer precise descriptions of consistency behavior, but they require expertise and specialized tools to apply to real software systems. In this paper, we propose and describe consistency oracles, an alternative way of specifying the consistency model of a system that provides interactive answers, making them easier and more flexible to use in a variety of ways. A consistency oracle mimics the interface of a distributed storage system, but returns all possible values that may be returned under a given consistency model. This allows consistency oracles to be directly applied in the testing and verification of both distributed storage systems and the client software that uses those systems. Beom Heyn Kim, Sukwon Oh, David Lie |
HotOS | 3 |
| 2017 | Glimmers: Resolving the Privacy/Trust QuagmireabstractUsers today enjoy access to a wealth of services that rely on user-contributed data, such as recommendation services, prediction services, and services that help classify and interpret data. The quality of such services inescapably relies on trustworthy contributions from users. However, validating the trustworthiness of contributions may rely on privacy-sensitive contextual data about the user, such as a user's location or usage habits, creating a conflict between privacy and trust: users benefit from a higher-quality service that identifies and removes illegitimate user contributions, but, at the same time, they may be reluctant to let the service access their private information to achieve this high quality. David Lie, Petros Maniatis |
HotOS | 1 |
| 2017 | Prochlo: Strong Privacy for Analytics in the CrowdabstractThe large-scale monitoring of computer users' software activities has become commonplace, e.g., for application telemetry, error reporting, or demographic profiling. This paper describes a principled systems architecture---Encode, Shuffle, Analyze (ESA)---for performing such monitoring with high utility while also protecting user privacy. The ESA design, and its Prochlo implementation, are informed by our practical experiences with an existing, large deployment of privacy-preserving software monitoring. Andrea Bittau, Úlfar Erlingsson, Petros Maniatis, Ilya Mironov, Ananth Raghunathan, David Lie, Mitch Rudominer, Ushasree Kode, Julien Tinnés, Bernhard Seefeld |
SOSP | 6 |
| 2016 | LMP: light-weighted memory protection with hardware assistance
Wei Huang 0027, Zhen Huang 0002, Dhaval Miyani, David Lie |
ACSAC | 4 |
| 2016 | IntelliDroid: A Targeted Input Generator for the Dynamic Analysis of Android Malware
Michelle Y. Wong, David Lie |
NDSS | 2 |
| 2016 | Talos: Neutralizing Vulnerabilities with Security Workarounds for Rapid ResponseabstractThere is often a considerable delay between the discovery of a vulnerability and the issue of a patch. One way to mitigate this window of vulnerability is to use a configuration workaround, which prevents the vulnerable code from being executed at the cost of some lost functionality -- but only if one is available. Since application configurations are not specifically designed to mitigate software vulnerabilities, we find that they only cover 25.2% of vulnerabilities. To minimize patch delay vulnerabilities and address the limitations of configuration workarounds, we propose Security Workarounds for Rapid Response (SWRRs), which are designed to neutralize security vulnerabilities in a timely, secure, and unobtrusive manner. Similar to configuration workarounds, SWRRs neutralize vulnerabilities by preventing vulnerable code from being executed at the cost of some lost functionality. However, the key difference is that SWRRs use existing error-handling code within applications, which enables them to be mechanically inserted with minimal knowledge of the application and minimal developer effort. This allows SWRRs to achieve high coverage while still being fast and easy to deploy. We have designed and implemented Talos, a system that mechanically instruments SWRRs into a given application, and evaluate it on five popular Linux server applications. We run exploits against 11 real-world software vulnerabilities and show that SWRRs neutralize the vulnerabilities in all cases. Quantitative measurements on 320 SWRRs indicate that SWRRs instrumented by Talos can neutralize 75.1% of all potential vulnerabilities and incur a loss of functionality similar to configuration workarounds in 71.3% of those cases. Our overall conclusion is that automatically generated SWRRs can safely mitigate 2.1× more vulnerabilities, while only incurring a loss of functionality comparable to that of traditional configuration workarounds. Zhen Huang 0002, Mariana D'Angelo, Dhaval Miyani, David Lie |
IEEE Symposium on Security and Privacy | 4 |
| 2015 | SPSM 2015: 5th Annual ACM CCS Workshop on Security and Privacy in Smartphones and Mobile DevicesabstractThe 2015 SPSM (Security and Privacy in Smartphones and Mobile Devices) workshop is designed to bring together researchers focusing on smartphones. It is a single day workshop co-located with ACM CCS (Conference on Computer and Communications Security) 2015, designed to provide a venue for interested researchers and practitioners to get together and exchange ideas. Glenn Wurster, David Lie |
CCS | 2 |
| 2015 | Caelus: Verifying the Consistency of Cloud Services with Battery-Powered DevicesabstractCloud storage services such as Amazon S3, Drop Box, Google Drive and Microsoft One Drive have become increasingly popular. However, users may be reluctant to completely trust a cloud service. Current proposals in the literature to protect the confidentiality, integrity and consistency of data stored in the cloud all have shortcomings when used on battery-powered devices -- they either require devices to be on longer so they can communicate directly with each other, rely on a trusted service to relay messages, or cannot provide timely detection of attacks. We propose Caelus, which addresses these shortcoming. The key insight that enables Caelus to do this is having the cloud service declare the timing and order of operations on the cloud service. This relieves Caelus devices from having to record and send the timing and order of operations to each other -- instead, they need to only ensure that the timing and order of operations both conforms to the cloud's promised consistency model and that it is perceived identically on all devices. In addition, we show that Caelus is general enough to support popular consistency models such as strong, eventual and causal consistency. Our experiments show that Caelus can detect consistency violations on Amazon's S3 service when the desired consistency requirements set by the user are stricter than what S3 provides. Caelus achieves this with a roughly 12.6% increase in CPU utilization on clients, 1.3% of network bandwidth overhead and negligible impact on the battery life of devices. Beom Heyn Kim, David Lie |
IEEE Symposium on Security and Privacy | 2 |
| 2014 | Ocasta: Clustering Configuration Settings for Error RecoveryabstractEffective machine-aided diagnosis and repair of configuration errors continues to elude computer systems designers. Most of the literature targets errors that can be attributed to a single erroneous configuration setting. However, a recent study found that a significant amount of configuration errors require fixing more than one setting together. To address this limitation, Ocasta statistically clusters dependent configuration settings based on the application's accesses to its configuration settings and utilizes the extracted clustering of configuration settings to fix configuration errors involving more than one configuration settings. Ocasta treats applications as black-boxes and only relies on the ability to observe application accesses to their configuration settings. We collected traces of real application usage from 24 Linux and 5 Windows desktops computers and found that Ocasta is able to correctly identify clusters with 88.6% accuracy. To demonstrate the effectiveness of Ocasta, we evaluated it on 16 real-world configuration errors of 11 Linux and Windows applications. Ocasta is able to successfully repair all evaluated configuration errors in 11 minutes on average and only requires the user to examine an average of 3 screenshots of the output of the application to confirm that the error is repaired. A user study we conducted shows that Ocasta is easy to use by both expert and non-expert users and is more efficient than manual configuration error troubleshooting. Zhen Huang 0002, David Lie |
DSN | 2 |
| 2012 | PScout: analyzing the Android permission specificationabstractModern smartphone operating systems (OSs) have been developed with a greater emphasis on security and protecting privacy. One of the mechanisms these systems use to protect users is a permission system, which requires developers to declare what sensitive resources their applications will use, has users agree with this request when they install the application and constrains the application to the requested resources during runtime. As these permission systems become more common, questions have risen about their design and implementation. In this paper, we perform an analysis of the permission system of the Android smartphone OS in an attempt to begin answering some of these questions. Because the documentation of Android's permission system is incomplete and because we wanted to be able to analyze several versions of Android, we developed PScout, a tool that extracts the permission specification from the Android OS source code using static analysis. PScout overcomes several challenges, such as scalability due to Android's 3.4 million line code base, accounting for permission enforcement across processes due to Android's use of IPC, and abstracting Android's diverse permission checking mechanisms into a single primitive for analysis. Kathy Wain Yee Au, Yi Fan Zhou, Zhen Huang 0002, David Lie |
CCS | 4 |
| 2011 | Unicorn: two-factor attestation for data securityabstractMalware and phishing are two major threats for users seeking to perform security-sensitive tasks using computers today. To mitigate these threats, we introduce Unicorn, which combines the phishing protection of standard security tokens and malware protection of trusted computing hardware. The Unicorn security token holds user authentication credentials, but only releases them if it can verify an attestation that the user's computer is free of malware. In this way, the user is released from having to remember passwords, as well as having to decide when it is safe to use them. The user's computer is further verified by either a TPM or a remote server to produce a two-factor attestation scheme. We have implemented a Unicorn prototype using commodity software and hardware, and two Unicorn example applications (termed as uApps, short for Unicorn Applications), to secure access to both remote data services and encrypted local data. Each uApp consists of a small, hardened and immutable OS image, and a single application. Our Unicorn prototype co-exists with a regular user OS, and significantly reduces the time to switch between the secure environment and general purpose environment using a novel mechanism that removes the BIOS from the switch time. Mohammad Mannan, Beom Heyn Kim, Afshar Ganjali, David Lie |
CCS | 4 |
| 2011 | Patch auditing in infrastructure as a service cloudsabstractA basic requirement of a secure computer system is that it be up to date with regard to software security patches. Unfortunately, Infrastructure as a Service (IaaS) clouds make this difficult. They leverage virtualization, which provides functionality that causes traditional security patch update systems to fail. In addition, the diversity of operating systems and the distributed nature of administration in the cloud compound the problem of identifying unpatched machines. Lionel Litty, David Lie |
VEE | 2 |
| 2010 | Kivati: fast detection and prevention of atomicity violationsabstractBugs in concurrent programs are extremely difficult to find and fix during testing. In this paper, we propose Kivati, which can efficiently detect and prevent atomicity violation bugs. Kivati imposes an average run-time overhead of 19%, which makes it practical to deploy on software in production environments. The key attribute that allows Kivati to impose this low overhead is its use of hardware watchpoints, which can be found on most commodity processors. Kivati combines watchpoints with a simple static analysis that annotates regions of codes that likely need to be executed atomically. The watchpoints are then used to monitor these regions for interleaving accesses that may lead to an atomicity violation. When an atomicity violation is detected, Kivati dynamically reorders the access to prevent the violation from occurring. Kivati can be run in prevention mode, which optimizes for performance, or in bug-finding mode, which trades some performance for an enhanced ability to find bugs. Lee Chew, David Lie |
EuroSys | 2 |
| 2010 | Dude, Where's That IP? Circumventing Measurement-based IP Geolocation
Phillipa Gill, Yashar Ganjali, Bernard Wong 0001, David Lie |
USENIX Security Symposium | 4 |
| 2009 | Computer Meteorology: Monitoring Compute Clouds
Lionel Litty, H. Andrés Lagar-Cavilla, David Lie |
HotOS | 3 |
| 2008 | Augmenting Counterexample-Guided Abstraction Refinement with Proof TemplatesabstractExisting software model checkers based on predicate abstraction and refinement typically perform poorly at verifying the absence of buffer overflows, with analyses depending on the sizes of the arrays checked. We observe that many of these analyses can be made efficient by providing proof templates for common array traversal idioms idioms, which guide the model checker towards proofs that are independent of array size. We have integrated this technique into our software model checker, PtYasm, and have evaluated our approach on a set of testcases derived from the Verisec suite, demonstrating that our technique enables verification of the safety of array accesses independently of array size. Thomas E. Hart, Kelvin Ku, Arie Gurfinkel, Marsha Chechik, David Lie |
ASE | 5 |
| 2008 | PtYasm: Software Model Checking with Proof TemplatesabstractWe describe PTYASM, an enhanced version of the YASM software model checker which uses proof templates. These templates associate correctness arguments with common programming idioms, thus enabling efficient verification. We have used PTYASM to verify the safety of array accesses in programs derived from the Verisec suite. PTYASM is able to verify this property in the majority of testcases, while existing software model checkers fail to do so due to loop unrolling. Thomas E. Hart, Kelvin Ku, Arie Gurfinkel, Marsha Chechik, David Lie |
ASE | 5 |
| 2008 | Security Benchmarking using Partial Verification
Thomas E. Hart, Marsha Chechik, David Lie |
HotSec | 3 |
| 2008 | Hypervisor Support for Identifying Covertly Executing Binaries
Lionel Litty, H. Andrés Lagar-Cavilla, David Lie |
USENIX Security Symposium | 3 |
| 2007 | Relaxed Determinism: Making Redundant Execution on Multiprocessors Practical
Jesse Pool, Ian Sin Kwok Wong, David Lie |
HotOS | 3 |
| 2007 | A buffer overflow benchmark for software model checkersabstractSoftware model checking based on abstraction-refinement has recently achieved widespread success in verifying API conformance in device drivers, and we believe this success can be replicated for the problem of buffer overflow detection. This paper presents a publicly-available benchmark suite to help guide and evaluate this research. The benchmark consists of 298 code fragments of varying complexity capturing 22 buffer overflow vulnerabilities in 12 open source applications. We give a preliminary evaluation of the benchmark using the SatAbs model checker Kelvin Ku, Thomas E. Hart, Marsha Chechik, David Lie |
ASE | 4 |
| 2007 | Quantifying the Strength of Security Systems
David Lie, Mahadev Satyanarayanan |
HotSec | 1 |
| 2006 | Splitting Interfaces: Making Trust Between Applications and Operating Systems Configurable
Richard Ta-Min, Lionel Litty, David Lie |
OSDI | 3 |
| 2006 | Using VMM-based sensors to monitor honeypotsabstractVirtual Machine Monitors (VMMs) are a common tool for implementing honeypots. In this paper we examine the implementation of a VMM-based intrusion detection and monitoring system for collecting information about attacks on honeypots. We document and evaluate three designs we have implemented on two open-source virtualization platforms: User-Mode Linux and Xen. Our results show that our designs give the monitor good visibility into the system and thus, a small number of monitoring sensors can detect a large number of intrusions. In a three month period, we were able to detect five different attacks, as well as collect and try 46 more exploits on our honeypots. All attacks were detected with only two monitoring sensors. We found that the performance overhead for monitoring such intrusions is independent of which events are being monitored, but depends entirely on the number of monitoring events and the underlying monitoring implementation. The performance overhead can be significantly improved by implementing the monitor directly in the privileged code of the VMM, though at the cost of increasing the size of the trusted computing base of the system. Kurniadi Asrigo, Lionel Litty, David Lie |
VEE | 3 |
| 2003 | Implementing an untrusted operating system on trusted hardwareabstractRecently, there has been considerable interest in providing "trusted computing platforms" using hardware~---~TCPA and Palladium being the most publicly visible examples. In this paper we discuss our experience with building such a platform using a traditional time-sharing operating system executing on XOM~---~a processor architecture that provides copy protection and tamper-resistance functions. In XOM, only the processor is trusted; main memory and the operating system are not trusted.Our operating system (XOMOS) manages hardware resources for applications that don't trust it. This requires a division of responsibilities between the operating system and hardware that is unlike previous systems. We describe techniques for providing traditional operating systems services in this context.Since an implementation of a XOM processor does not exist, we use SimOS to simulate the hardware. We modify IRIX 6.5, a commercially available operating system to create xomos. We are then able to analyze the performance and implementation overheads of running an untrusted operating system on trusted hardware. David Lie, Chandramohan A. Thekkath, Mark Horowitz |
SOSP | 1 |
| 2003 | Specifying and Verifying Hardware for Tamper-Resistant SoftwareabstractWe specify a hardware architecture that supports tamper-resistant software by identifying an "idealized" model, which gives the abstracted actions available to a single user program. This idealized model is compared to a concrete "actual" model that includes actions of an adversarial operating system. The architecture is verified by using a finite-state enumeration tool (a model checker) to compare executions of the idealized and actual models. In this approach, software tampering occurs if the system can enter a state where one model is inconsistent with the other in performing the verification, we detected a replay attack scenario and were able to verify the security of our solution to the problem. Our methods were also able to verify that all actions in the architecture are required, as well as come up with a set of constraints on the operating system to guarantee liveness for users. David Lie, John C. Mitchell, Chandramohan A. Thekkath, Mark Horowitz |
S&P | 1 |
| 2001 | A simple method for extracting models for protocol codeabstractThe use of model checking for validation requires that models of the underlying system be created. Creating such models is both difficult and error prone and as a result, verification is rarely used despite its advantages. In this paper, we present a method for automatically extracting models from low level software implementations. Our method is based on the use of an extensible compiler system, xg++, to perform the extraction. The extracted model is combined with a model of the hardware, a description of correctness, and an initial state. The whole model is then checked with the Murφ model checker. As a case study, we apply our method to the cache coherence protocols of the Stanford FLASH multiprocessor. Our system has a number of advantages. First, it reduces the cost of creating models, which allows model checking to be used more frequently. Second, it increases the effectiveness of model checking since the automatically extracted models are more accurate and faithful to the underlying implementation. We found a total of 8 errors using our system. Two errors were global resource errors, which would be difficult to find through any other means. We feel the approach is applicable to other low level systems. David Lie, Andy Chou, Dawson R. Engler, David L. Dill |
ISCA | 1 |
| 2000 | Architectural Support for Copy and Tamper Resistant SoftwareabstractAlthough there have been attempts to develop code transformations that yield tamper-resistant software, no reliable software-only methods are know. This paper studies the hardware implementation of a form of execute-only memory (XOM) that allows instructions stored in memory to be executed but not otherwise manipulated. To support XOM code we use a machine that supports internal compartments---a process in one compartment cannot read data from another compartment. All data that leaves the machine is encrypted, since we assume external memory is not secure. The design of this machine poses some interesting trade-offs between security, efficiency, and flexibility. We explore some of the potential security issues as one pushes the machine to become more efficient and flexible. Although security carries a performance penalty, our analysis indicates that it is possible to create a normal multi-tasking machine where nearly all applications can be run in XOM mode. While a virtual XOM machine is possible, the underlying hardware needs to support a unique private key, private memory, and traps on cache misses. For efficient operation, hardware assist to provide fast symmetric ciphers is also required. David Lie, Chandramohan A. Thekkath, Mark Mitchell, Patrick Lincoln, Dan Boneh, John C. Mitchell, Mark Horowitz |
ASPLOS | 1 |