Collaborative Research: SaTC: CORE: Small: Mixed Assurance Reasoning via Modal Logic

The safety, security, and reliability of software applications have far-reaching impacts on everyone’s lives; therefore, formal reasoning about these guarantees has become increasingly important. While formal verification provides the highest assurance, very few companies can afford the cost of it. On the other hand, lower-effort approaches such as testing, applying linting tools, and peer code review have been widely adopted in the industry. In addition, a complex system may include differently analyzed components: some are tested, some go through a static analysis, while others undergo code review. This project aims to answer the question of how to formally reason about the safety, reliability, and security assurances of such complex systems when heterogeneous analysis methods are applied. Further, this project investigates, in the event of an incident, how counterfactual reasoning can be applied to identifying the cause of the issue and refine or harden the analyses or software to prevent future incidents. This project provides training opportunities for undergraduate and graduate students in topics including program testing, verification, vulnerability detection, and software security via research projects and dedicated course modules. The project first develops the logical and semantic foundations for compositional assurance reasoning, where modal operators such as possibility and necessity are used to express truth derived from under-approximate (incomplete) analysis and truth derived from over-approximate (complete) analysis, respectively. Reasoning principles to compose results from different types of analysis are built around these modal operators. To be concretely applicable to the analysis of programs for assurance, a Kripke semantics based on the program execution semantics is defined to give meaning to the logical formulas. Next, this project develops counterfactual reasoning principles to aid the refinement of the analysis and repairing programs when an incident occurs. The expressiveness, effectiveness, and efficiency of the reasoning systems are evaluated via case studies drawn from security incidents reported in recent years. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.