A5011704924- Security and Verification in Computing
- Physical Unclonable Functions (PUFs) and Hardware Security
- Distributed systems and fault tolerance
- Advanced Malware Detection Techniques
- Cryptographic Implementations and Security
- Parallel Computing and Optimization Techniques
- Radiation Effects in Electronics
- Cloud Computing and Resource Management
- Chaos-based Image/Signal Encryption
- Natural Language Processing Techniques
- Anomaly Detection Techniques and Applications
- Interconnection Networks and Systems
- Software System Performance and Reliability
- Topic Modeling
University of California, San Diego
2017-2021
UC San Diego Health System
2019
We present pretend synchrony , a new approach to verifying distributed systems, based on the observation that while programs must execute asynchronously, we can often soundly treat them as if they were synchronous when their correctness. To do so, compute synchronization semantically equivalent program where all sends, receives, and message buffers, have been replaced by simple assignments, yielding be verified using Floyd-Hoare style Verification Conditions SMT. implement our framework for...
We introduce Blade, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. Blade is built on the insight that stop via execution, it suffices cut dataflow expressions speculatively secrets ( sources ) those leak them through cache sinks ), rather than prohibit speculation altogether. formalize this in static type system (1) types each expression as either transient , i.e., possibly containing or being stable (2) prohibits by requiring all sink...
We introduce canonical sequentialization, a new approach to verifying unbounded, asynchronous, message-passing programs at compile-time. Our builds upon the following observation: due combinatorial explosion in complexity, programmers do not reason about their systems by case-splitting over all possible execution orders. Instead, correct tend be well-structured so that programmer can small number of representative executions, which we call program’s sequentialization. have implemented our...
To be secure, cryptographic algorithms crucially rely on the underlying hardware to avoid inadvertent leakage of secrets through timing side channels. Unfortunately, such channels are ubiquitous in modern hardware, due its labyrinthine fast-paths and optimizations. A promising way vulnerabilities is devise --- verify conditions under which a design free variability, i.e., executes constant-time. In this paper, we present Iodine: clock precise, constant-time approach eliminating hardware....
We present Xenon, a solver-aided, interactive method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic designs by drastically reducing the effort needed localize root cause of verification failures via new notion constant-time counterexamples, which uses synthesize minimal set secrecy assumptions an loop. To reduce time exploits modularity code module summaries, thereby avoiding duplicate work across multiple instantiations. show how Xenon's...
We present Xenon, a solver-aided method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic designs by drastically reducing the effort needed localize root cause of verification failures via new notion constant-time counterexamples, which uses automatically synthesize minimal set secrecy assumptions. further exploits modularity code module summaries, thereby avoiding duplicate work across multiple instantiations. show how Xenon's assumption...