Re: [seL4] seL4 on unverified ARM platforms

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? In the future, are there plans to automatically generate the relevant code? Just wondering. Sincerely, Demi