Automated verification of properties of concurrent, distributed and parallel specifications with applications to computer security

With NPRP project 09-1107-1-168 (ending in February 2014), we have outlined the foundations of a framework for representing Concurrent, Distributed and Parallel (CDP) languages and explored methodologies to formally prove properties about their computations. CDP languages are important as they underlie many of today’s key technologies, such as cloud computing, web programming, security assurance and multi-processor compilation. We expanded substructural operational semantics (SSOS) to effectively specify most of their constructs, and developed a methodology that scales up proof techniques routinely applied to sequential language to CDP languages. Our case studies have demonstrated the elegance and promise of this approach, highlighted several advantages over current proof techniques, and provided preliminary evidence that these foundations can be leveraged in practice. We carried out these case studies in CLF, a framework that supports SSOS specifications effectively. In the proposed next phase of the project, we are interested in applying the above methodological and technical insights to CDP languages and systems of practical importance. One focus will be the specification and verification of secure systems, specifically electronic voting, web-based languages, and cryptographic protocols. This will be accompanied with an extension of the current CLF prototype with developing meta-reasoning support for expressing properties of such specifications and for validating their proofs.