Analysis and Enforcement of Properties in Software Systems.
Degree: PhD, Electrical and Computer Engineering, 2019, Virginia Tech
Due to the lack of effective techniques for detecting and mitigating property violations, existing
approaches to ensure the safety and security of software systems are often labor intensive and error prone. Furthermore, they focus primarily on functional correctness of the software code while
ignoring micro-architectural details of the underlying processor, such as cache and speculative
execution, which may undermine their soundness guarantees.
To fill the gap, I propose a set of new methods and tools for ensuring the safety and security of
software systems. Broadly speaking, these methods and tools fall into three categories. The first
category is concerned with static program analysis. Specifically, I develop a novel abstract interpre
tation framework that considers both speculative execution and a cache model, and guarantees to be sound for estimating the execution time of a program and detecting side-channel information leaks. The second category is concerned with static program transformation. The goal is to eliminate side channels by equalizing the number of CPU cycles and the number of cache misses along all program paths for all sensitive variables. The third category is concerned with runtime safety enforcement. Given a property that may be violated by a reactive system, the goal is to synthesize an enforcer, called the shield, to correct the erroneous behaviors of the system instantaneously, so that the property is always satisfied by the combined system. I develop techniques to make the shield practical by handling both burst error and real-valued signals.
The proposed techniques have been implemented and evaluated on realistic applications to demonstrate their effectiveness and efficiency.
Advisors/Committee Members: Schaumont, Patrick Robert (committeechair), Meng, Na (committee member), Jung, Changhee (committee member), Wang, Chao (committee member), Hsiao, Michael S. (committee member), Zeng, Haibo (committee member).
Subjects/Keywords: Shield Synthesis; Program Analysis; Timing Side Channel; Cache Timing Leak; Speculative Execution; Abstract Interpretation
to Zotero / EndNote / Reference
APA (6th Edition):
Wu, M. (2019). Analysis and Enforcement of Properties in Software Systems. (Doctoral Dissertation). Virginia Tech. Retrieved from http://hdl.handle.net/10919/90887
Chicago Manual of Style (16th Edition):
Wu, Meng. “Analysis and Enforcement of Properties in Software Systems.” 2019. Doctoral Dissertation, Virginia Tech. Accessed July 20, 2019.
MLA Handbook (7th Edition):
Wu, Meng. “Analysis and Enforcement of Properties in Software Systems.” 2019. Web. 20 Jul 2019.
Wu M. Analysis and Enforcement of Properties in Software Systems. [Internet] [Doctoral dissertation]. Virginia Tech; 2019. [cited 2019 Jul 20].
Available from: http://hdl.handle.net/10919/90887.
Council of Science Editors:
Wu M. Analysis and Enforcement of Properties in Software Systems. [Doctoral Dissertation]. Virginia Tech; 2019. Available from: http://hdl.handle.net/10919/90887