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.

• I don't understand. Whether a USB device can manipulate the memory space of a process actually depends as much on the operating system than on the device itself. You can't prove/check this without testing the entire chain, including the OS. So what would be the role of a digital logic simulator in this equation? A virtualization tool like QEMU, in which you would add your simulated USB device, would make more sense to me. And electronics actually plays little role here. But maybe I'm missing something.
– dim
Feb 9, 2017 at 20:30