On 11/21/20 8:26 PM, Heiser, Gernot (Data61, Kensington NSW) wrote:

On 20 Nov 2020, at 03:28, Demi M. Obenour wrote:

...

The first is an explanation for why the restrictions stated are acceptable. For instance, it is clear that the targeted systems are static. Why is dynamism not required? Is it because these systems are created with a single purpose in mind, and so do not need the level of extensibility that a dynamic system offers?

As the design document states: It’s meant to be simple but sufficient for the target domains. More generality means more complexity. The proposed model should serve almost all present use cases. Even Cog System’s “ultra-secure phone" fits this model: All the dynamicism, such as run-time installable apps, happen inside a virtual machine with an Android guest. From the seL4 PoV, the phone is a simple, static architecture with a fixed number of protected components: the “use VM” containing a full Android system with virtual drivers, the VMM, a console, a I/O multiplexing component, a “driver VM” (which should eventually become individual driver components), a network encryption component and a storage encryption VM. If the Platform supports this use case, it will definitely support most others.

That makes sense. Would it be possible to include a “non-goals” section, for the benefit of readers who have not attended the seL4 Summit?

For the (presently very small) class of deployments that need more generality, a different framework is needed. Such more general frameworks may be standardised in the future (and may or may not be extensions of the Core Platform), but for now this is not the aim. If you want a system where a fully general OS is needed, Genode is likely your best choice (at the expense of losing most of the assurance).

That’s understandable. A fully general OS is a far more difficult task, even if it does not attempt to conform to POSIX or other legacy standards. It certainly does not belong in “a first step”.

...

The second is the ability to forcibly reset a protection domain to its initial state. […]

As the RFC clearly spells out, this is “a first step”, we won’t get very far trying to boil the ocean. Re-initialising components is definitely planned, but for a future release (see the last few minutes of my talk at the seL4 Summit: https://www.youtube.com/watch?v=khcjH77riGA&list=PLtoQeavghzr1Z3mF5B-f_xnFm81MPPwA-&index=4 https://www.youtube.com/watch?v=khcjH77riGA&list=PLtoQeavghzr1Z3mF5B-f_xnFm81MPPwA-&index=4).

Indeed, “boiling the ocean” is not a good place to start. One last question: will cross-core communications channels be allowed?

Gernot

Sincerely, Demi

On 11/21/20, Heiser, Gernot (Data61, Kensington NSW) wrote:

As the design document states: It’s meant to be simple but sufficient for the target domains. More generality means more complexity. The proposed model should serve almost all present use cases. Even Cog System’s “ultra-secure phone" fits this model: All the dynamicism, such as run-time installable apps, happen inside a virtual machine with an Android guest. From the seL4 PoV, the phone is a simple, static architecture with a fixed number of protected components: the “use VM” containing a full Android system with virtual drivers, the VMM, a console, a I/O multiplexing component, a “driver VM” (which should eventually become individual driver components), a network encryption component and a storage encryption VM. If the Platform supports this use case, it will definitely support most others.

Of course, in a system that runs a legacy general-purpose OS in a VM on top of a static system, only applications that are specifically written to use the secure APIs can actually be properly secured (and that's assuming that the secure static part of the system is actually capable of doing what the application needs). An seL4-native general purpose OS could apply the same security model to everything, including unmodified applications for legacy OSes assuming it provides a compatible environment, albeit at the very likely expense of formal verification of most OS components and subsystems above the kernel. However, even a mostly-unverified microkernel OS should still be considerably more secure than a legacy OS assuming the design is remotely reasonable.

On 11/22/20, Heiser, Gernot (Data61, Kensington NSW) wrote:

Yes. While this is a reasonable use case, it’s not one we see happening. Very few real-world systems are built from scratch, they almost inevitably are an evolution of something existing. And, compared to pulling out critical assets to run native (as in the Cog phone), the additional security gain from running *everything* native is small, compared to the huge refactoring/porting effort. That’s why just about everyone opts for the HACMS-style incremental cyber retrofit, as Cog have done it.

But if you think you gain enough by going fully native on an unverified microkernel OS, then Genode is what you should use. If you want high assurance for your critical assets, then the seL4 Core Platform is the way to go (at least once it supports VMs).

I'm (still) working on UX/RT, my own implementation of a QNX-like OS based on seL4, which I've posted about here in the past. It will use code from existing free Unices wherever possible. This includes using the LKL project to run multiple kernel-only Linux systems as servers to provide device drivers, disk filesystems, and a network stack. Most of the "regular" user-mode tools and libraries will be forked or ported from Linux and BSD. Many Linux-specifc API functions will be natively supported (making it easier to implement a Linux binary compatibility environment as well as porting Linux applications). I'm certainly not attempting to build a full-featured Unix-like system from scratch by myself because that would be a lot of reinvention of the wheel. Much of what I need is already out there. I just need to fill in the gaps. Basically, I'm intending to make a general-purpose Unix-like microkernel OS that is practical for most use cases where legacy Unices (including Linux) are currently used, while hopefully being more secure and easier to manage than any legacy Unix, and still maintaining a reasonable degree of backwards compatibility (and also following the Unix philosophy, or at least my interpretation of it, considerably better than any other modern system).

On Nov 22, 2020, at 10:01, Demi M. Obenour wrote:

(Speaking of avionics: is it possible to scale formal verification to systems of that scale? I would love to see formally-verified avionics software.)

Inria and Airbus have had success doing this since at least ~2005. If you want to read about this, Sandrine Blazy and Xavier Leroy have discussed it in some prior publications. Today I believe this process is supported commercially by the company AbsInt.

On Nov 22, 2020, at 10:43, Demi M. Obenour wrote:

On 11/22/20 1:36 PM, Matthew Fernandez wrote:

...

...

On Nov 22, 2020, at 10:01, Demi M. Obenour wrote:

(Speaking of avionics: is it possible to scale formal verification to systems of that scale? I would love to see formally-verified avionics software.)

Inria and Airbus have had success doing this since at least ~2005. If you want to read about this, Sandrine Blazy and Xavier Leroy have discussed it in some prior publications. Today I believe this process is supported commercially by the company AbsInt.

Is this full functional verification, or “merely” proving freedom from runtime errors? (Quotes because proving freedom from runtime errors is still a substantial victory.)

That I do not know. You would have to read their papers or ask the authors.

On 11/22/20 2:56 AM, Andrew Warkentin wrote:

On 11/21/20, Heiser, Gernot (Data61, Kensington NSW) wrote:

...

As the design document states: It’s meant to be simple but sufficient for the target domains. More generality means more complexity. The proposed model should serve almost all present use cases. Even Cog System’s “ultra-secure phone" fits this model: All the dynamicism, such as run-time installable apps, happen inside a virtual machine with an Android guest. From the seL4 PoV, the phone is a simple, static architecture with a fixed number of protected components: the “use VM” containing a full Android system with virtual drivers, the VMM, a console, a I/O multiplexing component, a “driver VM” (which should eventually become individual driver components), a network encryption component and a storage encryption VM. If the Platform supports this use case, it will definitely support most others.

Of course, in a system that runs a legacy general-purpose OS in a VM on top of a static system, only applications that are specifically written to use the secure APIs can actually be properly secured (and that's assuming that the secure static part of the system is actually capable of doing what the application needs). An seL4-native general purpose OS could apply the same security model to everything, including unmodified applications for legacy OSes assuming it provides a compatible environment, albeit at the very likely expense of formal verification of most OS components and subsystems above the kernel. However, even a mostly-unverified microkernel OS should still be considerably more secure than a legacy OS assuming the design is remotely reasonable.

Do you believe that an seL4-native general-purpose OS is practical? I certainly hope so! What do you believe such an OS would look like? Regarding security, I mostly agree with you, but I do have one caveat to point out. There is a distinction between assurance (essentially, correctness) and security. For instance, a legacy VM can still be very secure if there is no way for untrusted data to enter it, or if its interactions with untrusted data are extremely limited. That’s how QubesOS works, and it has proven to be quite successful. In the case of QubesOS, this has allowed Linux-native desktop environments (such as XFCE and KDE) to be used in security-critical areas. This in turn allows for a much better user experience than would otherwise be possible given the project’s resources, and has been critical in QubesOS’s success in the desktop space. Sincerely, Demi