We're extremely pleased to announce a major milestone...

All posts seL4's posts Post Back to profile

We're extremely pleased to announce a major milestone in the history of seL4: The proof of functional correctness for the 64-bit Arm architecture (AArch64) is complete!
Congratulations Proofcraft on this awesome achievement!
We're immensely grateful to UK's National Cyber Security Centre for for funding this work, which is of great importance to the seL4 ecosystem.
You now no longer have to chose between a verified kernel and a modern processor, you can have both 😁
https://sel4.systems/news/#aarch64-fc

Like 21 April at 7:40 | Open on fosstodon.org

9 comments

Gernot Heiser

@sel4 So glad to see this finally done! :done: :fireworks:

21 April at 7:46 | Open on discuss.systems

johnz

@gernot @sel4 that's a great achievement, well done!

22 April at 1:26 | Open on fosstodon.org

Marce Coll

@sel4 it is mind boggling to me that this can be achieved, what an incredible work

21 April at 10:09 | Open on functional.cafe

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 | Open on mastodon.social

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 https://sel4.systems/Info/more-research.html