Email or username:

Password:

Forgot your password?
All posts seL4's posts Post Back to profile
Top-level
Tariq

@sel4

I'm no expert so I have a question.

Is this a proof that the software behaves as intended on the specified hardware regarding input and output?

Or is it a proof that no vulnerabilities exist - eg side effects from a given input/output pair?

21 April at 16:50 | Wall-to-wall | Open on mastodon.social
2 comments
Felix Neumann

@rzeta0 @sel4

The functional correctness proof is what you described, that the actual implementation behaves as specified.

Now, the specification has certain properties (that can be mathematically proven). For example, that memory can’t be accessed or processes can‘t communicate without authorization.

One of the topics still being worked on is protection against covert channels (like Spectre).

I recommend reading sel4.systems/Info/more-researc

22 April at 18:15 | Open on hachyderm.io
Gernot Heiser

@rzeta0 @sel4 "functional correctness" means the kernel always behaves to spec, no matter what you feed it.

23 April at 6:04 | Open on discuss.systems
Go Up