Carnegie Mellon University in Qatar
IT University of Copenhagen
Supported by the Qatar National Research Fund

Meta-CLF 2

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

Project Description

Concurrent, distributed and parallel (CDP) computing has played an important role in our society for over 40 years. Indeed, computations and devices that combine independent threads of execution (concurrency), that run on more than one place at once (distribution), and that execute several steps at the same time (parallelism) span the gamut from hardware chips to operating systems and networking middleware to high-level applications such as database management systems. Ensuring that CDP programs are correct is notoriously difficult: in addition to the "normal" bugs found in sequential programming, programmers also need to deal with race conditions, deadlocks, livelocks and other undesirable side-effects that come along the benefits of asynchronicity. Programmers must also worry about their applications being immune from a plethora of security vulnerabilities.
CLF, a type-theoretic logical framework based on a large fragment of linear logic, is a new approach to representing and reasoning about CDP languages and systems. Because CLF internalizes concurrency (rather than simulating it), it allows simple and elegant specifications of numerous concurrent formalism. CLF specifications are executable and can effortlessly be run in the Celf system. Expressing properties of CLF specifications requires a meta-language that manipulates CLF objects. In the past, we have produced hand-written proofs of these properties. These proofs are extremely concise as they internalize the sausage-making of concurrency.
This project wants to build an environment where proving properties of CDP systems becomes a practical proposition, eventually for users with little knowledge of logic or type theory. Specifically, we propose to develop an automated tool to verify CDP properties written in CLF, to build such a tool, and to apply it to a much broader range of systems than we have done in the past. Such case studies will focus on security-sensitive languages and systems, both for their practicality and because their often short specification concentrates extremely complex forms of concurrent reasoning.
This work was funded by the Qatar National Research Fund as project NPRP 7-988-1-178 (Automated verification of properties of concurrent, distributed and parallel specifications with applications to computer security) for an amount of $898,420 over 3 years.



Past members


(none yet)

Related Work