Task 2.4: Algorithmic techniques for Dependability and Security

[Halderman, Sangiovanni-Vincentelli, Seshia]

TerraSwarm system properties typically fall into three categories:

1. purely computational (e.g., invariants on control programs),
2. purely physical (e.g., properties of the physical plant), or
3. cyber-physical (e.g., involving physical quantities such as real time, power, energy, acceleration, and velocity, whose values depend on both computational and physical components of the system).

In this task, we will focus on formal verification and security analysis of the cyber-physical properties of TerraSwarm systems. First, this task evaluates communication protocols proposed or used for distributed systems for their ability to preserve security and privacy. The task develops appropriate security mechanisms for use with these protocols, recognizing the diversity of security requirements. Second, the task verifies the cyber-physical properties of software implementations of these protocols. For example, timing and energy consumption of a network of TerraSwarm nodes and services such as clock synchronization or routing can create vulnerabilities and/or be used to mitigate vulnerabilities. Given the dynamic nature of a TerraSwarm system, such verification will be based on combining systematic measurements with model inference from observations. The approach will be to combine assume-guarantee reasoning, techniques to identify (conditional) independence of different components, and combinations of inductive learning and deductive procedures.