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 ap...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on computer-aided design of integrated circuits and systems 2021-01, Vol.40 (1), p.143-156
Main Authors: Shayan, Mohammed, Bhattacharjee, Sukanta, Wille, Robert, Chakrabarty, Krishnendu, Karri, Ramesh
Format: Article
Language:English
Subjects:
Biochips
Checkpointing
Computer security
control systems
Cyber-physical systems
Drugs
Electrodes
fluid flow control
fluidics
industry applications
Microfluidics
Monitoring
Protocol (computers)
Safety critical
Security
Software
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0278-0070
1937-4151
DOI:10.1109/TCAD.2020.2988351