Reasoning about Reliability and Security Using Boolean Methods

Опубликовано 6 сентября 2016, 5:29

Detecting and correcting errors before run-time is increasingly important in today's ubiquitous computing environment. Decision procedures for first-order logics are widely applicable in design verification and program analysis. However, as existing procedures do not scale up, verification methods sacrifice modeling precision for scalability. Imprecise modeling often results in numerous false alarms and the inability to verify properties that depend on data or timing, in addition to control. I will present an approach that addresses this problem by modeling with first-order logics involving arithmetic and reasoning using new, efficient decision procedures for those logics. In our approach, decision problems involving arithmetic are transformed to problems in the Boolean domain, such as Boolean satisfiability solving, thereby leveraging recent advances in that area. The transformation automatically detects and exploits problem structure based on new theoretical results and machine learning. I will describe the underlying theory and present experimental results showing that our decision procedures outperform other state-of-the-art procedures by over a factor of 100. The decision procedures form the computational engines for two verification systems, UCLID and TMV. These systems have been applied to problems in computer security, electronic design automation, and software engineering that require efficient and precise analysis of data- and timing-dependent properties; for example, a semantics-aware detector of viruses and worms has shown far greater resilience to obfuscation than commercial tools.