TY - JOUR
T1 - How Secure Are Checkpoint-Based Defenses in Digital Microfluidic Biochips?
AU - Shayan, Mohammed
AU - Bhattacharjee, Sukanta
AU - Wille, Robert
AU - Chakrabarty, Krishnendu
AU - Karri, Ramesh
N1 - Funding Information:
Manuscript received December 17, 2019; revised February 22, 2020; accepted April 6, 2020. Date of publication April 16, 2020; date of current version January 11, 2021. This work was supported in part by the Army Research Office under Grant W911NF-17-1-0320, in part by NSF under Award CNS-1833622 and Award CNS-1833624, in part by the New York University Center for Cyber Security (CCS), and in part by New York University Abu Dhabi Center for Cyber Security (CCS-AD). This article was recommended by Associate Editor S. Chakraborty. (Corresponding author: Mohammed Shayan.) Mohammed Shayan and Ramesh Karri are with the Department of Electrical and Computer Engineering, New York University, Brooklyn, NY 11201 USA (e-mail: mos283@nyu.edu; rkarri@nyu.edu).
Publisher Copyright:
© 1982-2012 IEEE.
PY - 2021/1
Y1 - 2021/1
N2 - 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.
AB - 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.
KW - Computer security
KW - control systems
KW - fluid flow control
KW - fluidics
KW - industry applications
KW - microfluidics
KW - security
UR - http://www.scopus.com/inward/record.url?scp=85083699350&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85083699350&partnerID=8YFLogxK
U2 - 10.1109/TCAD.2020.2988351
DO - 10.1109/TCAD.2020.2988351
M3 - Article
AN - SCOPUS:85083699350
SN - 0278-0070
VL - 40
SP - 143
EP - 156
JO - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
JF - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
IS - 1
M1 - 9069286
ER -