Towards Accessible Integrated Formal Reasoning Environments for Protocol Design

[PDF]

Abstract

Computer science researchers in the programming languages and formal verification communities have produced a variety of automated tools and techniques for assisting formal reasoning tasks. However, while there exist notable successes in utilizing these tools to develop safe and secure software and hardware, both leading-edge advances and basic techniques (such as model checking, state space search, type checking, logical inference and verification, computation of congruence closures, non-interference enforcement, and so on) remain underutilized by large populations of end-users that may benefit from them when they engage in formal reasoning tasks within their own application domains. This may be in part because (1) these tools and techniques are not readily accessible to endusers who are not experts in formal systems or are simply not aware of what is available and how it can be utilized, and (2) these tools and techniques are only valuable when used in conjunction with one another and with appropriate domain-specific libraries and databases. Motivated by these circumstances, we present our ongoing efforts, built on earlier work in developing user-friendly formal verification tools, to develop a platform for assembling, instantiating, and deploying user-friendly, interactive, integrated formal reasoning environments that can assist users engaged in routine domain-specific formal reasoning tasks in application domains. This infrastructure encompasses a programming language, compilers, and other tools for building up from components, instantiating with domain-specific formal content, and finally delivering such environments in the form of ready-to-use web-based applications that can run entirely within a standard web browser. We describe current efforts to use this platform to instantiate an environment the application domain of correct network protocol design.