On 2020-01-22 22:22, Klein, Gerwin (Data61, Kensington NSW) wrote: > >> On 23 Jan 2020, at 12:40, Demi M. Obenour <[email protected]> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
