In low level information flow analysis, each variable is usually assigned a security level. The basic model comprises two distinct levels: low and high, meaning, respectively, publicly observable information, and secret information. To ensure confidentiality, flowing information from high to low variables should not be allowed. On the other hand, to ensure integrity, flows to high variables should be restricted. We are working on the broad area of reasonng about information-flow security policies using hyperproperties. This includes verification, monitoring, synthesis, and testing.

The vehicle routing problem (VRP) is one of the most studied combinatorial optimization problems and is concerned with the optimal design of routes to be used by a fleet of vehicles to service a set of customers. With the growing popularity of autonomous vehicles (e.g., driverless cars and unmanned aerial systems) in the modern world, there is pressing need to revisit this problem in the context of decentralized multi-agent systems. We are developing distributed algorithms that attempt to optimize the global cost of routes for a set of autonomous vehicles.

Runtime monitoring and enforcement of desirable properties is an effective technique that ensures correctness at execution time. Runtime monitoring is particularly useful in large systems, where exhaustive analysis is not practical and conventional testing may fail to identify complex corner cases. The challenging problem in this area is to implement resource-efficient runtime monitors that do not intervene in the normal execution of the program under inspection. We are conducting research on automated design and development of runtime monitors for distributed real-time systems that (1) need to provide certain security and privacy policies and (2) take into consideration resource constraints (e.g., power, time budget, CPU cycles, memory, etc), while effectively exploiting the heterogeneous nature of today's computing platforms, such as many-core GPUs and multi-core processors.

Model-based software development advocates the system design flow as a chain of steps starting from a high-level specification and leading to an implementation on a given execution platform. It involves the use of methods and tools for progressively deriving the implementation by making adequate design choices and step-by-step transformations that terminate when a correct-by-construction implementation is obtained. We are developing a novel framework for automated implementation of parallel/distributed real-time applications that are correct-by-construction from an abstract model specified in terms of a set of heterogeneous components, synchronization primitives, and priority rules for scheduling purposes. Our approach is based on algorithmic transformation techniques. These algorithms take as input a model of system processes and generate as output distributed and/or multi-threaded code, while ensuring that the execution of the code is observationally equivalent to the input abstract model and, hence, all the functional properties of the high-level model are preserved.

ASSESS

Assess (Automated Synthesizer for SElf-Stabilizing Systems) implements a set of SMT-based techniques to synthesize distributed self-stabilizing programs. It takes as input (1) the topology of the distributed system in terms of read/write restrictions of processes, (2) the legitimate behavior of the system in the absence of faults, and (3) a set of high-level requirements such as the timing model (asynchronous or synchronous), and stabilization type (weak, strong, or monotonic). The legitimate behavior is specified either explicitly as a state predicate LS, or implicitly as a set of LTL formulas. The tool returns a finite-state self-stabilizing protocol as a set of guarded commands that realize the input specification. The synthesis engine of ASSESS is SMT-based and the tool supports the SMT-solver Z3 and the model finder Alloy. The internal algorithm are sound and complete, meaning that a synthesized solution by Assess is correct by construction and if the tool fails to synthesize a solution, then there does not exist one.

RiTHM

The tool RiTHM (Runtime Time-triggered Heterogeneous Monitoring) takes a C program under inspection and a set of LTL properties as input and generates an instrumented C program that is verified at run time by a time-triggered monitor. The output C program can be instrumented in two ways: (1) it is monitored in a time-triggered fashion with a fixed polling period, or (2) the monitor is augmented with PID or fuzzy controllers that ensure minimum variation in monitor polling period while maximizing memory utilization. In both cases, the monitor is invoked in a time-triggered fashion, ensuring that the states of the program can be reconstructed at each invocation by using efficient instrumentation. The monitor verification decision procedure is sound and complete and takes advantage of the GPU many-core technology to speedup monitoring and reduce the runtime overhead.

SYCRAFT

Sycraft (SYmboliC synthesizeR and Adder of Fault-Tolerance) is a tool for transforming distributed fault-intolerant programs to distributed fault-tolerant programs. In Sycraft, a distributed fault-intolerant program is specified in terms of a set of processes and an invariant. Each process is specified as a set of actions in a guarded command language, a set of variables that the process can read, and a set of variables that the process can write. The issue of distribution is addressed in shared-memory model where processes are constrained by their ability in reading and writing program variables. Given a set of fault actions and a safety specification, the tool synthesizes a fault-tolerant program via a symbolic implementation of respective synthesis algorithms. Sycraft has successfully been used to synthesize some of the classic protocols in the literature of fault-tolerant computing in distributed systems (e.g., Byzantine agreement, token ring, etc.).