| Title | : | Formal Analysis of Intel SGX Enclaves |
| Speaker | : | Dr, Mohit Jangid (Ohio State University, Columbus) |
| Details | : | Mon, 23 Sep, 2024 3:00 PM @ SSB 233 (MR1), CSE D |
| Abstract: | : | Abstract: Software and protocol development has followed the design-develop-break-patch cycle for many years. One resolution to mitigate such a persistent cycle is to build the systems with formal analysis following the "analysis-prior-to-development" philosophy. At present, state space explosion and the limited expressibility of formal model languages limit the scalability and efficiency of this approach. Expanding the scope of formal methods to broader cases requires augmented modeling and a deeper understanding of the underlying operating mechanisms. In particular, by modeling with a precise system environment and refined adversary capabilities, I wish to expand the boundaries of formal methods, exposing limiting root causes and opening novel paths for improvement. For example, considering how concurrent execution influences the processes; modeling a granular access control for user and adversary groups; incorporating human interactions; allowing adversaries to control program execution at the instruction level; and trading off between literal cryptographic accuracy and modeled theory imprecisions augments the formal modeling to reason about unconventional properties. Apart from raising security assurance, such comprehensive coverage of the system environment and precise adversary capability expand the utility of formal methods to large systems and facilitate the derivation of unconventional properties. Additionally, such design provides further feedback to formal tool development to design targeted building blocks that improve the efficiency, scalability, and expressibility of formal modeling. In this thesis, I will first present an enhanced and generic formal analysis of the trusted execution environment (TEE) technology—Intel Software Guard Extension. In particular, I made a first attempt to extend formal verification to program logic for SGX enclaves with the powerful SGX threat model. In this effort, I derived state continuity properties with respect to three heterogeneous trusted computing modules. Next, I propose an in-depth formal investigation of the widely deployed, challenging, and long Bluetooth pairing protocols. Here, I have incorporated precise access control with human interaction and a combination of different protocols together to derive a complex multi-session attack. Such enhanced modeling for Bluetooth allowed us to drive other attacks resulting from static variable reuse, multi-threading, reflection, human error, and compromise devices from one unified model. Overall, in my talk, I will present challenges and insights learned while applying formal methods to security and privacy. In the future, I aim to improve and automate security and privacy verification by incorporating machine learning to guide Tamarin's proof search process and enhance scalability. Additionally, to improve privacy-capturing techniques, I propose formalizing Allowlist privacy attacks using process algebra to articulate better capturing of observational equivalence. Short Bio: Dr. Mohit Kumar Jangid received PhD in Cybersecurity from The Ohio State University, Columbus, in 2024. After completing B. Tech. from MNIT Jaipur in 2013, he worked as a software engineer at MAQ Software, Hyderabad, India. Mohit is interested in fundamental and automated security solutions that can scale to large complex systems and provide comprehensive coverage beyond human reasoning ability. He is interested in automated formal verification, system security and privacy, cryptography, and protocol design. He received a Graduate Student Research award for his thesis research in 2024. He was chosen for the Sesquicentennial Student Scholar Leadership Program and was awarded a scholarship for his vision to serve back in India. He played various roles in student leadership and global engagement programs at The Ohio State University. Apart from academics, he enjoys sports, music, and painting. He values spirituality and practices meditation and mindfulness as an integral part of his life. |
