Research





Synthesizing Stealthy Attacks on Cardiac Devices

An Implantable Cardioverter Defibrillator (ICD) is a medical device for the detection of fatal cardiac arrhythmias and their treatment through electrical shocks intended to restore normal heart rhythm. An ICD reprogramming attack seeks to alter the device parameters to induce unnecessary therapy or prevent required therapy.

We present a formal approach for the synthesis of ICD reprogramming attacks that are both effective, i.e., lead to fundamental changes in the required therapy, and stealthy, i.e., are hard to detect. We focus on the discrimination algorithm underlying Boston Scientific devices (one of the principal ICD manufacturers) and formulate the synthesis problem as one of multi-objective optimization. Our solution technique is based on an Optimization Modulo Theories (OMT) encoding of the problem and allows us to derive device parameters that are optimal with respect to the effectiveness-stealthiness tradeoff. Our method can be tailored to the patients current condition, and generalizes to unseen signals.


Synthesizing Stealthy Attacks on Cardiac Devices
Top: cardiac signals (intracardiac electrograms). Bottom: ICD discrimination under nominal (non-attacked) and reprogrammed (attacked) parameters. With nominal parameters, the ICD delivers arrhytmia-terminating shock therapy (T), while attacked parameters prevent therapy.

SMT-based synthesis of safe and robust digital controllers

We present a new method for the automated synthesis of digital controllers with formal safety guarantees for systems with nonlinear dynamics, noisy output measurements, and stochastic disturbances. Our method derives digital controllers such that the corresponding closed-loop system, modeled as a sampled-data stochastic control system, satisfies a safety specification with probability above a given threshold. The method alternates between two steps: generation of a candidate controller (sub-optimal but rapid to generate), and verification of the candidate. The candidate is found by maximizing a Monte Carlo estimate of the safety probability, and by simulating the system with a non-validated ODE solver. To rule out unstable candidate controllers, we prove and utilize Lyapunov indirect method for instability of sampled-data nonlinear systems. In the verification step, we use a validated solver based on SMT to compute a numerically and statistically valid confidence interval for the safety probability of the candidate controller. If such probability is not above the threshold, we expand the search space for candidates by increasing the controller degree. We evaluate our technique on three case studies: an artificial pancreas model, a powertrain control model, and a quadruple-tank process.


SMT-based synthesis of safe and robust digital controllers
Blood glucose levels under basal insulin therapy (left) and synthesized controller (right).

Robust design synthesis for probabilistic systems

We consider the problem of synthesizing optimal and robust designs (given as parametric Markov chains) that are 1) robust to pre-specified levels of variation in the system parameters; 2) satisfy strict performance, reliability and other quality constraints; and 3) are Pareto optimal with respect to a set of quality optimisation criteria.

The resulting Pareto front consists of quality attribute regions induced by the parametric designs (see picture). The size and shape of these regions provide key insights into the system robustness since they capture the sensitivity of quality attributes to parameter changes (i.e, small regions = robust designs).

The method is implemented in the RODES tool and is based on a combination of GPU-accelerated parameter synthesis for Markov chains (to compute the quality attribute regions for fixed discrete parameters) through the PRISM-PSY tool, and multi-objective optimization based on an extended, sensitivity-aware dominance relation.


Robust design synthesis for probabilistic systems
Sensitivity-aware Pareto front for the Google File System model. Through an extended Pareto dominance relation we can include designs that are slightly suboptimal but with improved robustness (in red).

Precise parameter synthesis for continuous-time Markov chains

Given a parameteric continuous-time Markov chain (pCTMC), we aim at finding parameter values such that a CSL property is guaranteed to hold (threshold synthesis), or, in the case of quantitative properties, the probability of satisfying the property is maximised or minimised (max synthesis).

The solution of the threshold synthesis (see picture) is a decomposition of the parameter space into true and false regions that are guaranteed to, respectively, satisfy and violate the property, plus an arbitrarily small undecided region. On the other hand, in the max synthesis problem we identify an arbitrarily small region guaranteed to contain the actual maximum/minimum.

We developed synthesis methods based on a parameteric extension of probabilistic model checking to compute probability bounds, as well as refinement and sampling of the parameter space. We implemented GPU-accelerated algorithms for synthesis in the PRISM-PSY tool, which we applied to a variety of biological and engineered systems, including models of molecular walkers, mammalian cell cycle, and the Google file system.


Precise parameter synthesis for continuous-time Markov chains
Parameter ranges and bounds (vertical axis) for the probability of infection extinction in an epidemic model. Green: true region, i.e., with probability above the desired threshold (transparent plane). Red: false region. Yellow: undecided region.

Optimal synthesis of stochastic chemical reaction networks

The automatic derivation of Chemical Reaction Networks (CRNs) with prescribed behavior is one of the holy grails of synthetic biology, allowing for design automation of molecular devices and in the construction of predictive biochemical models.

In this work, we provide the first method for optimal syntax-guided synthesis of stochastic CRNs that is able to derive not just rate parameters but also the structure of the network. Borrowing from the programming language community, we propose a sketching language for CRNs that allows to specify the network as a partial program, using holes and variables to capture unknown components. Under the Linear Noise Approximation of the chemical master equation, a CRN sketch has a semantics in terms of parametric Ordinary Differential Equations (ODEs).

We support rich correctness properties that describe the temporal profile of the network as constraints over mean and variance of chemical species, and their higher order derivatives. In this way, we can synthesize networks where e.g., one of the species exhibit a bell-shape profile or has variance greater than its expectation.

We synthesize CRNs that satisfies the sketch constraints and a correctness specification while minimizing a given cost function (capturing the structural complexity of the network). The optimal synthesis algorithm employs SMT solvers over reals and ODEs (iSAT) and a meta-sketching abstraction that speeds up the search through cost constraints.

We evaluate the approach on a three key problems: synthesis of networks with a bell-shaped profile (occurring in signaling cascades), a CRN implementation of a stochastic process with prescribed levels of noise and synthesis of sigmoidal profiles in the phosphorelay network.


Optimal synthesis of stochastic chemical reaction networks
Top: correctness specification describing the sigmoid/switch-like profile of the final layer in a phosphorelay cascade. The specification requires that the species exhibit an inflection point (at any time). Bottom: species concentrations in the synthesized network.

Hardware-in-the-loop energy optimization

Energy efficiency of cardiac pacemakers is crucial because it reduces the frequency of device re-implantations, thus improving the quality of life of cardiac patients.

To achieve effective energy optimisation, we take a hardware-in-the-loop (HIL) simulation approach: the pacemaker model is encoded into hardware and interacts with a computer simulation of the heart model. In addition, a power monitor is attached to the pacemaker to provide real-time power consumption measurements. The approach is model-based and supports generic control systems. Controller (e.g., pacemaker) and plant (e.g., heart) models are specified as networks of parameterised timed input/output automata (using MATLAB Stateflow) and translated into executable code.

We realise a fully automated optimisation workflow, where HIL simulation is used to build a probabilistic power consumption model from power measurement data. The obtained model is used by the optimisation algorithm to find optimal pacemaker parameters that e.g., minimise consumption or maximise battery lifetime. We additionally employ parameter synthesis methods to restrict the search to safe parameters. We employ timed Petri nets as an intermediate representation of the executable specification, which facilitates efficient code generation and fast simulations.


Video demonstration of HIL energy optimization

SMT-based synthesis of gene regulatory networks

Unraveling the structure and the logic of gene regulation is crucial to understand how organisms develop and so is the derivation of predictive models able to reproduce experimental observations and explain unknown biological interactions.

This research centers on the synthesis of biological programs, with specific focus on Boolean gene regulatory networks (GRN). We developed methods based on the idea of synthesis by sketching, which enables explicit modeling of hypotheses and unknown information, specified as e.g. choices or uninterpreted functions. Through the formalization as an SMT problem, the method can automatically and efficiently resolve the unknown information in order to obtain a model that is consistent with observations.

We applied this approach to synthesize the first GRN model of the sea urchin embryo (an important model organism in biology) that precisely and fully reproduce available temporal and spatial expression data and the effects of perturbation experiments. The data we used is the result of 30+ years of research in the Davidson lab at Caltech.


SMT-based synthesis of gene regulatory networks
Synthesis of gene networks. Input: partial gene expression data and uncertain model. Output: synthesized model that reproduces known data and resolves missing data.

Parameter synthesis for pacemaker design optimization

Verification is useful in establishing key correctness properties of cardiac pacemakers, but has limitations, in that it is not clear how to redesign the model if it fails to satisfy a given property. Instead, parameter synthesis aims to automatically find optimal values of parameters to guarantee that a given property is satisfied.

In this project, we develop methods to synthesize pacemaker parameters that are safe, robust and, at the same time, able to optimise a given quantitative requirement such as energy consumption or clinical indicators. We solve this problem by combining symbolic methods (SMT solving) for ruling out parameters that violate heart safety (red areas in the figure) with evolutionary strategies for optimising the quantitative requirement.


Parameter synthesis for pacemaker design optimization
Synthesis by bilevel optimization. Right: the maximal robust parameter (blue) is the center of the largest cube (light blue) without counter-examples (red). Left: in a bilevel problem, the domain of the outer problem is the solution space of the inner problem.