On 23 Jan 2020, at 14:05, Demi M. Obenour wrote:

On 2020-01-22 22:22, Klein, Gerwin (Data61, Kensington NSW) wrote:

...

...

On 23 Jan 2020, at 12:40, Demi M. Obenour wrote:

My understanding is that seL4 is currently only verified for one particular ARM platform. Is it considered production-ready on other ARM boards?

There are two current ARM verification configurations, one for standard ARMv7 Sabre, and one with hardware virtualisation support for the TK1 board.

For most ARMv7 boards without hardware virtualisation, the verification will either still apply or should be very simple to adjust (1-2h to a few days of work max), as long as only the values of a few hardware constants change. The same probably applies to boards with hardware virtualisation support, but there tends to be more to adjust, and we haven’t updated the verification for these yet very often, so I don’t have much data no that.

Cheers, Gerwin

Good to know, thanks! Obviously, the lack of SMMU support will be a blocker in many cases, but it is good to know that seL4 can be ported to other boards without too much effort. Are there plans to port the verification to additional boards if there is demand and funding?

Yes, we have done that in the past, and it can be done again. Ironically, supporting a new board for an existing architecture is probably much more work on the implementation side than the verification side, because on the implementation side you have to discover what those constants are and how that new board works, often without good hardware docs (plus you will usually want additional user-space drivers etc for that board). The verification takes much of the hardware interface as assumption, and as long as the constants satisfy fairly basic conditions, things will often “just work”. What is hard to add are significant new features like SMMU.

In the future, are there plans to automatically generate the relevant code? Just wondering.

Indeed, we do have such plans, but we’re currently pretty flat out on the verification side on delivering the verification for RISC-V and the mixed-criticality features. Once there is a bit of that mythical breathing space, I would very much like to add a proper platform interface to the verification stack that gets its input directly from the cmake config files and can be checked offline quickly for “will the verification work with this”. Currently the config comes into the verification stack manually, and is checked eventually against reality via the pre-processed C constants. I don’t think all that is very hard, but it will require re-organising the proofs a bit, and turning implicit properties of these constants into an explicit interface. It could even be a good starter project for someone who would like to get into the formal verification side of things. Should have done it this way from the beginning, but of course all of this started as a research project on something that people said couldn’t be done at all, so supporting multiple platforms efficiently was not the first thing on our minds back then ;-) Cheers, Gerwin