0
\$\begingroup\$

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.

enter image description here

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.

\$\endgroup\$
1
  • 1
    \$\begingroup\$ 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. \$\endgroup\$
    – dim
    Feb 9, 2017 at 20:30

1 Answer 1

Reset to default
2
\$\begingroup\$

I think that this kind of question would be a better fit on the Information Security or Computer Science sites.

They'll probably explain how your model is overly simplistic. USB is a complex protocol, and the host drivers and applications that deal with it are complex, too. There are many ways to attack a system if you can get it to execute code of your choosing.

\$\endgroup\$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .