Mohammed Shayan, S. Bhattacharjee, Robert Wille, Krishnendu Chakrabarty, Ramesh Karri,
"How Secure are Checkpoint-based Defenses in Digital Microfluidic Biochips? IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems (TCAD)"
, in IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems (TCAD), 2020, ISSN: 1937-4151
Original Titel:
How Secure are Checkpoint-based Defenses in Digital Microfluidic Biochips? IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems (TCAD)
Sprache des Titels:
Englisch
Original Kurzfassung:
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 cyberphysical
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. Existing solutions either rely on probabilistic security analysis that does not
consider all possible actions an attacker may use to overcome an
applied checkpoint 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 work, we address this issue
by developing an exact method, which uses the deductive power of
satisfiability solvers to verify whether a checkpoint-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 checkpoint scheme.
Sprache der Kurzfassung:
Englisch
Journal:
IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems (TCAD)
Forschungs-