Re: [seL4] seL4 on unverified ARM platforms

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