We're doing a bachelor's degree project about formal methods applied to external hardware security. In practice I wonder how much we can abstract and simplify a model of external hardware specifically USB that is connected to a host, typically a USB device external memory that is connected via a USB interconnection to a USB host such as a computer system.
Our objective is to theoretically prove and/or formally model a security for external hardware devices when such are connected to a computer.
I have drawn the following model and I'm looking for tools that could actually test and check the model so that we can perform model checking.
We want to check that a connected external USB cannot manipulate a "protected" user process ("UP") by some means.
Our basic theory looks today like this.
Conf ∧ ⊨ Model USB ∧ ⊭ WRITE
The above theory should mean that if the configuration is done, the external hardware cannot write and cannot manipulate a user process.
Would this question be appropriate for you or somewhere else around? Specifically I wonder which tool (Quartus ModelSim? Logisim?) could be used to actually check our model or which theorem-prover could be used to actually prove our theory?
We want to simplify and still keep a realistic model.