CAREER: A Semantic Framework for Verifying Heterogeneous Applications

The computing landscape has been gradually shifting from monolithic to distributed systems, catering to, for example, cloud computing and Internet of Things (IoT) applications. This shift challenges the development of such applications because they no longer may act autonomously but have to interact with other, concurrently running components in an orchestrated way, following intended protocols.

A compounding factor challenging the understanding of the behaviors of such applications is their heterogeneity: rather than being developed in one common programming language, an array of languages is used, with some components of applications being actual physical objects. The project's novelties are the development of a framework for verifying compliance of these heterogeneous systems with the intended protocols of interactions between them, and the application of the framework to the verification of IoT systems.

The project's impacts are (a) foundational reasoning techniques that cater to the heterogeneity of today's systems, allowing not only guarantees of software written in multiple languages, but also of software that interacts with untrusted objects such as sensors; (b) a novel case study of the use of the techniques in verifying a practical system; and (c) the training and development of graduate and undergraduate students.

The verification framework uses linear session types to define semantic logical relations for protocol compliance and resource management and explores two scenarios: trusted environments and untrusted environments. The environments convey, respectively, whether an application developer may or may not assume that the foreign objects with which they interact are well-behaved.

Possible applications to validate the framework, for both scenarios, include validation of properties such as parametricity and noninterference, as well as IoT applications. While semantic logical relations enjoy popularity overall, only recently have they been introduced to the session-typed setting by the investigator. The project addresses how semantic logical relations express various desirable properties, such as confluence, deadlock freedom, and resource management, which traditionally have been expressed syntactically using types.

The project not only intends to scale session type theory to new application domains but also develops techniques that serve as a stepping stone for the development of more general reasoning frameworks such as fully dependent session type theories.

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.