How Secure Are Checkpoint-Based Defenses in Digital Microfluidic Biochips?

A digital microfluidic biochip (DMFB) is a miniaturized laboratory capable of implementing biochemical protocols. Fully integrated DMFBs consist of a hardware platform, controller, and network connectivity, making it a cyber-physical system (CPS). A DMFB CPS is being advocated for safety-critical applications, such as medical diagnosis, drug development, and personalized medicine. Hence, the security of a DMFB CPS is of immense importance to their successful deployment. Recent research has made progress in devising corresponding defense mechanisms by employing so-called checkpoints (CPs). Existing solutions either rely on probabilistic security analysis that does not consider all possible actions an attacker may use to overcome an applied CP mechanism or rely on exhaustive monitoring of DMFB at all time-steps during the assay execution. For devising a defense scheme that is guaranteed to be secure, an exact analysis of the security of a DMFB is needed. This is not available in the current state-of-the-art. In this article, we address this issue by developing an exact method, which uses the deductive power of satisfiability solvers to verify whether a CP-based defense thwarts the execution of an attack. We demonstrate the usefulness of the proposed method by showcasing two applications on practical bioassays: 1) security analysis of various checkpointing strategies and 2) derivation of a counterexample-guided fool-proof secure CP scheme.