Comment by msdz
9 hours ago
Are timing (over network) attacks, physical access, etc. typically excluded from research like this for being “out of scope”, so to speak? I’m not familiar.
9 hours ago
Are timing (over network) attacks, physical access, etc. typically excluded from research like this for being “out of scope”, so to speak? I’m not familiar.
Mathematical proofs tend to assume that they are built on perfect foundations (you have to stop the proof somewhere!). Unfortunately, proving that the software is correct just means you need to find a flaw in a deeper layer.
They aren't out of scope as much as they are irrelevant. It has been a best practice to ensure that the things you would be attempting to attack the timing of do not let you do this for a very long time. We are so far down this road that we do things like generate thousands of values and throw most of them away to mitigate the laziest attempts at what would be considered in scope.
It's still relevant (and probably also rather difficult) to prove that seL4 itself conforms to those best practices.