Analysis and Enforcement of Properties in Software Systems
| dc.contributor.author | Wu, Meng | en |
| dc.contributor.committeechair | Schaumont, Patrick R. | en |
| dc.contributor.committeemember | Meng, Na | en |
| dc.contributor.committeemember | Jung, Changhee | en |
| dc.contributor.committeemember | Wang, Chao | en |
| dc.contributor.committeemember | Hsiao, Michael S. | en |
| dc.contributor.committeemember | Zeng, Haibo | en |
| dc.contributor.department | Electrical and Computer Engineering | en |
| dc.date.accessioned | 2019-07-03T08:02:09Z | en |
| dc.date.available | 2019-07-03T08:02:09Z | en |
| dc.date.issued | 2019-07-02 | en |
| dc.description.abstract | 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 interpretation 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. | en |
| dc.description.abstractgeneral | It is important for everything around us to follow some rules to work correctly. That is the same for our software systems to follow the security and safety properties. Especially, softwares may leak information via unexpected ways, e.g. the program timing, which makes it more difficult to be detected or mitigated. For instance, if the execution time of a program is related to the sensitive value, the attacker may obtain information about the sensitive value. On the other side, due to the complexity of software, it is nearly impossible to fully test or verify them. However, the correctness of software systems at runtime is crucial for critical applications. While existing approaches to find or resolve properties violation problem are often labor intensive and error prone, in this dissertation, I first propose an automated tool for detecting and mitigating the security vulnerability through program timing. Programs processed by the tool are guaranteed to be time constant under any sensitive values. I have also taken the influence of speculative execution, which is the cause behind recent Spectre and Meltdown attack, into consideration for the first time. To enforce the correctness of programs at runtime, I introduce an extra component that can be attached to the original system to correct any violation if it happens, thus the entire system will still be correct. All proposed methods have been evaluated on a variety of real world applications. The results show that these methods are effective and efficient in practice. | en |
| dc.description.degree | Doctor of Philosophy | en |
| dc.format.medium | ETD | en |
| dc.identifier.other | vt_gsexam:19969 | en |
| dc.identifier.uri | http://hdl.handle.net/10919/90887 | en |
| dc.publisher | Virginia Tech | en |
| dc.rights | In Copyright | en |
| dc.rights.uri | http://rightsstatements.org/vocab/InC/1.0/ | en |
| dc.subject | Shield Synthesis | en |
| dc.subject | Program Analysis | en |
| dc.subject | Timing Side Channel | en |
| dc.subject | Cache Timing Leak | en |
| dc.subject | Speculative Execution | en |
| dc.subject | Abstract Interpretation | en |
| dc.title | Analysis and Enforcement of Properties in Software Systems | en |
| dc.type | Dissertation | en |
| thesis.degree.discipline | Computer Engineering | en |
| thesis.degree.grantor | Virginia Polytechnic Institute and State University | en |
| thesis.degree.level | doctoral | en |
| thesis.degree.name | Doctor of Philosophy | en |
Files
Original bundle
1 - 1 of 1