Attacking Formally Verified Software

[aeline]

Anyone hear been involved with red-teaming a system that had formally verified components? And if-so, what was the process like?

[gilmx]

Not a direct answer to your question, but I really enjoyed Joanna Rutkowska's blog entry on this topic (from a while back)

https://theinvisiblethings.blogspot.com/2010/05/on-formally-verified-microkernels-and.html

 

 

Edited November 8, 2022 by gilmx
add link

[aeline]

Thanks! Will read!

[bigmacjpg]

Is the system you will be testing built on bare metal ground up with formally verified components (kind of like what is described in the above blog post) or is it formally verified software running in a COTS OS? If the software is running in a non-formally verified OS (pretty much any COTS OS), I'd attack the OS and use that to get after the software. Also, is the software using any non-verified libraries under the covers? If so you could go after those libraries. I'm interested in what you are testing (prior to getting into cyber security I worked on safety critical systems using semi-formal methods, specifically Cleanroom software engineering).

[aeline]

Not actually working on anything on this atm, just interested in people's experience. I also work with formal methods. Obviously all formal methods has assumptions it builds on top of (it's not magic no-bug juice), but I was curious if anyone here had actually attacked a partially formalized system and what the experience was like.