Systems and methods for formal threat analysis of a smart healthcare system

1. A system for formal threat analysis of a smart healthcare system (SHS) that comprises an SHS database and at least one sensor collecting sensor data from at least one patient, the system comprising:

a processor; and

a machine-readable medium in operable communication with the processor and the SHS database, and having instructions stored thereon that, when executed by the processor, perform the following steps:

i) training a disease classification model (DCM) using the SHS database to generate DCM output data comprising at least one label for the at least one patient;

ii) training an anomaly detection model (ADM) using the SHS database to check consistency of the sensor data and to generate ADM output data;

iii) running an SHS decision control model, using the DCM output data and the ADM output data as input to the SHS decision control model, to generate SHS constraints;

iv) generating attack constraints based on a capability of a potential attacker and a goal of the potential attacker; and

v) running a satisfiability modulo theory (SMT) solver, using the SHS constraints, the attack constraints, and the sensor data as input to the SMT solver, to determine whether the goal of the potential attacker can be attained.

2. The system according to claim 1 , the instructions when executed further performing the following steps:

vi) if the goal of the potential attacker can be attained, generating an attack vector and reporting the attack vector to a user of the system; and

vii) if the goal of the potential attacker cannot be attained, increasing the capability of the potential attacker and running steps iv), v), vi), and vii) again.

3. The system according to claim 2 , further comprising a display in operable communication with the machine-readable medium, and

the reporting of the attack vector comprising displaying the attack vector on the display.

4. The system according to claim 2 , the at least one sensor comprising a plurality of sensors, and

the increasing the capability of the potential attacker comprising giving the potential attacker access to at least one additional sensor than the potential attacker had access to when step iv) was most recently performed.

5. The system according to claim 2 , the SMT solver first encoding the SHS constraints, the attack constraints, and the sensor data as a constraint satisfaction problem (CSP),

the SMT solver returning a result of satisfactory for the CSP if the goal of the potential attacker can be attained, and

the SMT solver returning a result of unsatisfactory for the CSP if the goal of the potential attacker cannot be attained.

6. The system according to claim 2 , step vi) further comprising, after generating the attack vector and reporting the attack vector, updating the goal of the potential attacker and running steps iv), v), vi), and vii) again, and stopping once the respective attack vector has been generated and reported for all goals of a predetermined number of goals of the potential attacker.

7. The system according to claim 1 , the SMT solver first encoding the SHS constraints, the attack constraints, and the sensor data as a constraint satisfaction problem (CSP),

the SMT solver returning a result of satisfactory for the CSP if the goal of the potential attacker can be attained, and

the SMT solver returning a result of unsatisfactory for the CSP if the goal of the potential attacker cannot be attained.

8. The system according to claim 1 , the DCM being a decision tree (DT) algorithm, a logistic regression (LR) algorithm, or a neural network (NN) algorithm.

9. The system according to claim 1 , the ADM being a density-based spatial clustering of applications with noise (DBSCAN) algorithm or a k-means algorithm.

10. The system according to claim 1 , the DCM being a DT algorithm and the ADM being a DBSCAN algorithm.

11. A method for formal threat analysis of a smart healthcare system (SHS) that comprises an SHS database and at least one sensor collecting sensor data from at least one patient, the method comprising:

i) training, by a processor in operable communication with the SHS database and the at least one sensor, a disease classification model (DCM) using the SHS database to generate DCM output data comprising at least one label for the at least one patient;

ii) training, by the processor, an anomaly detection model (ADM) using the SHS database to check consistency of the sensor data and to generate ADM output data;

iii) running, by the processor, an SHS decision control model, using the DCM output data and the ADM output data as input to the SHS decision control model, to generate SHS constraints;

iv) generating, by the processor, attack constraints based on a capability of a potential attacker and a goal of the potential attacker; and

v) running, by the processor, a satisfiability modulo theory (SMT) solver, using the SHS constraints, the attack constraints, and the sensor data as input to the SMT solver, to determine whether the goal of the potential attacker can be attained.

12. The method according to claim 11 , further comprising:

vi) if the goal of the potential attacker can be attained, generating an attack vector and reporting the attack vector to a user of the system; and

vii) if the goal of the potential attacker cannot be attained, increasing the capability of the potential attacker and running steps iv), v), vi), and vii) again.

13. The method according to claim 12 , the reporting of the attack vector comprising displaying the attack vector on a display in operable communication with the processor.

14. The method according to claim 12 , the at least one sensor comprising a plurality of sensors, and

the increasing the capability of the potential attacker comprising giving the potential attacker access to at least one additional sensor than the potential attacker had access to when step iv) was most recently performed.

15. The method according to claim 12 , the SMT solver first encoding the SHS constraints, the attack constraints, and the sensor data as a constraint satisfaction problem (CSP),

the SMT solver returning a result of satisfactory for the CSP if the goal of the potential attacker can be attained, and

the SMT solver returning a result of unsatisfactory for the CSP if the goal of the potential attacker cannot be attained.

16. The method according to claim 12 , step vi) further comprising, after generating the attack vector and reporting the attack vector, updating the goal of the potential attacker and running steps iv), v), vi), and vii) again, and stopping the method once the respective attack vector has been generated and reported for all goals of a predetermined number of goals of the potential attacker.

17. The method according to claim 11 , the DCM being a decision tree (DT) algorithm, a logistic regression (LR) algorithm, or a neural network (NN) algorithm.

18. The method according to claim 11 , the ADM being a density-based spatial clustering of applications with noise (DBSCAN) algorithm or a k-means algorithm.

19. The method according to claim 11 , the DCM being a DT algorithm and the ADM being a DBSCAN algorithm.

20. A system for formal threat analysis of a smart healthcare system (SHS) that comprises an SHS database and a plurality of sensors collecting sensor data from at least one patient, the system comprising: a processor; a display; a machine-readable medium in operable communication with the processor, the display, and the SHS database, and having instructions stored thereon that, when executed by the processor, perform the following steps: i) train a disease classification model (DCM) using the SHS database to generate DCM output data comprising at least one label for the at least one patient; ii) train an anomaly detection model (ADM) using the SHS database to check consistency of the sensor data and to generate ADM output data; iii) run an SHS decision control model, using the DCM output data and the ADM output data as input to the SHS decision control model, to generate SHS constraints; iv) generate attack constraints based on a capability of a potential attacker and a goal of the potential attacker; v) run a satisfiability modulo theory (SMT) solver, using the SHS constraints, the attack constraints, and the sensor data as input to the SMT solver, to determine whether the goal of the potential attacker can be attained; vi) if the goal of the potential attacker can be attained, generating an attack vector, reporting the attack vector to a user of the system, updating the goal of the potential attacker, and running steps iv), v), vi), and vii) again, and stopping once the respective attack vector has been generated and reported for all goals of a predetermined number of goals of the potential attacker; and vii) if the goal of the potential attacker cannot be attained, increasing the capability of the potential attacker and running steps iv), v), vi), and vii) again, the reporting of the attack vector comprising displaying the attack vector on the display, the increasing the capability of the potential attacker comprising giving the potential attacker access to at least one additional sensor than the potential attacker had access to when step iv) was most recently performed, the SMT solver first encoding the SHS constraints, the attack constraints, and the sensor data as a constraint satisfaction problem (CSP), the SMT solver returning a result of satisfactory for the CSP if the goal of the potential attacker can be attained, the SMT solver returning a result of unsatisfactory for the CSP if the goal of the potential attacker cannot be attained, the DCM being a decision tree (DT) algorithm, and the ADM being a DBSCAN algorithm.