STatic and Runtime ANalysis of Declarative Systems

A unified, declarative programming-based solution to system diagnosis

strands logo

STRANDS is a declarative programming-based framework for modeling, verifying and debugging a variety of types of systems — particularly distributed systems — allowing for static analysis of the system specification and runtime analysis of the system implementation.

STRANDS relies on Network Datalog (NDlog) for system modeling and programming. NDlog is a declarative programming language for network protocols, extending the classical query language Datalog.

Programming Logic

The user could use our Hoare-style programming logic developed for NDlog to specify and prove desirable properties about distributed systems. The proof can be performed with proof assistants (e.g., Coq)

Symbolic Execution

The user could specify and verify properties of distributed systems automatically using our static analyser, based on symbolic execution over declarative programs of network applications.

Compressed Provenance

The user could use the compressed provenance to record runtime system execution in a storage-efficient manner. This allows for future querying of the execution history during debugging.

Architecture

Publications

2016

  • Distributed Provenance Compression
    Chen Chen, Harshal Tushar Lehri, Lay Kuan Loh, Anupam Alur, Limin Jia, Boon Thau Loo, Wenchao Zhou
    To appear in SIGMOD, May 2017.
  • A Program Logic for Verifying Secure Routing Protocols
    Chen Chen, Limin Jia, Hao Xu, Cheng Luo, Wenchao Zhou and Boon Thau Loo
    Logical Methods in Computer Science, Volume 11, Issue 4, August 2016.

2015

2014

  • A Program Logic for Secure Routing Protocols
    Chen Chen, Limin Jia, Hao Xu, Cheng Luo, Wenchao Zhou and Boon Thau Loo
    34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE), June 2014.

Funding

NSF fundings

CNS-1218066; CNS-1117052; CNS-1115706; CNS-0845552; CNS-1453392; CNS- 1018061; NSFITR-1138996; ITR-1138996

Others

AFOSR Young Investigator Award FA9550-12-1-0327; AFOSR MURI ‘Science of Cyber Security: Modeling, Composition, and Measurement’.

Collaborators

Students

Chen Chen, PhD candidate, University of Pennsylvania
Lay Kuan Loh, PhD student, Carnegie Mellon University
Harshal Tushar Lehri, Master student, University of Pennsylvania
Anupam Alur, Master student, University of Pennsylvania
Hao Xu, Alumni Master student, University of Pennsylvania

Faculty

Boon Thau Loo, Associate Professor, University of Pennsylvania
Limin Jia, Assistant Research Professor, Carnegie Mellon University
Wenchao Zhou, Assistant Professor, Georgetown University