Hacker News Reader

Comment by mmooss | Hacker News Reader

SeL4 is old news - not a criticism, but has anyone added another formally proven layer or component? (Edit: I mean new components beyond the microkernel, not improvements to the microkernel.)

Also, I suspect some people - maybe some on HN :) - get emotional overload when they see the word 'proof' and their intellectual functions stop. It's not a panacea for the infinite problem of secure IT; it isn't a way to create or discover a perfect and flawless diamond of software. IIUC it means it's proven to meet specific requirements in specific conditions, and those requirements and conditions can be quite narrow; and it says nothing about other functions and conditions that are out of spec. Is that roughly correct?

What does it mean in practical terms? What does a security professional see when they see 'formally proven software'?

What are the specs that SeL4 meet (no, I haven't looked at the OP in a long time)? Isn't that the essential information here?

View on HN

Being "formally proven" to be free of various flaws did not make seL4 immune to memory corruption flaws. Despite the formal proof, a memory corruption flaw was found a few years ago. The PRs for the commits fixing it and amending seL4's proof are public:

https://github.com/seL4/seL4/pull/243

https://github.com/seL4/l4v/pull/453

You will find a number of other memory related bugs in its issue tracker:

https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...

Interestingly, the PR fixing "register clobbering" in memory was not labelled bug, so it is not listed when you filter by "bug".

I used to think seL4 was immune to these issues given its proof allegedly saying it is, but upon seeing this, I have come to think that the proof is not as comprehensive as the wider community has been lead to believe. That said, seL4 is still a very impressive piece of software.

Finally, to answer your question. The specification that seL4 meets is published on github:

https://github.com/seL4/l4v

I believe only certain versions and on certain architectures is seL4 verified for. There are no bugs found at the C source code level for these builds of seL4.

Even if it's not exactly seL4, there's good value in taking inspiration for design elements. It would still be a lot more robust than commodity operating systems.

This issue appears to have affected all architectures. This issue was present in the specification against which seL4 was verified. You can say that there are no bugs by virtue of it following the specification, but if the specification was wrong and in this case it was, then were there really no bugs?

There is always a specification, the question is "was this issue found against a version of seL4 that had been fully specified or not?".

I worked at the lab, I wasn't aware of any bug/issue on the fully specified kernel, that is why I am unsure if this counts or not.

I would need to have a look at the source code and proofs to confirm.

How does “This issue was present in the specification against which seL4 was verified” not imply yes to that question?

The PRs make it clear that this was a bug in the spec, and the implementation behaved according to spec.

That resulted in a memory corruption flaw in the C code. If you build a bridge to a specification and the bridge collapses, does saying that the specification was wrong in any way lessen the reality that the bridge failed?

Many bridges had to collapse until we learned how to build them.

As for seL4, the proofs (which are actually the state of the art in that field, yet definitely can be further perfected) are just one of the pillars supporting it e.g. the size of the TCB is another.

We do not give up on the goal because there was a mistake once. Nor is the goal not worthy; this is the absolute best the world has atm.

I did not suggest giving up, but I did suggest that seL4 is not immune to the bugs it’s advertising claims to avoid.

What's odd about this argument is that such bugs would be at risk of reintroduction in any other piece of software. Indeed, each release is expected to introduce new bugs and vendors typically sell service contracts based on the perpetual brokenness of existing software engineering processes. Whereas formally verified software typically has single digit numbers of bugs ... ever.

Sure, you get to score rhetorical points about the proof being incorrect once. But this bridge is now fixed and won't fail that way again in the same way.

Cartels and governments regularly hack phones and spy on and even kill activists. The current processes you are defending get people killed and are undermining civil society. SeL4 is a big deal and definitely worth the investments needed to make such reliability the norm instead of accepting the continual bridge collapses that occur in Linux land.

> Cartels and governments regularly hack phones and spy on and even kill activists.

Your comment implies SeL4 will prevent these things from happening. Isn't that going way too far?

It's a nice start, but we're nowhere near securing things on that level. Without looking into it, I'd put more faith in iPhone's lockdown mode.

We have a long way to crawl, but process isolation is the bedrock of all other security guarantees.

Tell me how process isolation prevents SQL injection. I could ask about any of a great variety of security issues, but I think SQL injection is a great choice for debunking “process isolation is the bedrock of all other security guarantees”. We do not have to worry because we have process isolation is basically this:

https://web.archive.org/web/20240123122515if_/https://www.sy...

I suspect you did not mean to say that, but your comments can be interpreted to mean that, especially when you suggest people will die if seL4 is not used as if nothing else matters, and inject that into a discussion of whether seL4’s is free of flaws (it is not).

Using seL4 is like flattening the ground on which a building foundation will sit. Just because the ground was flattened to within microns of flatness does not mean there is nothing else wrong with the foundation and building that are built on it.

Perhaps I am being pedantic, but you deserve this after suggesting the mere act of giving an opinion on seL4 made me an accessory to murder.

The systems we're talking about don't use SQL to communicate. They use data structures in a wire format of some sort because they are embedded systems. Don't pretend like we're talking about web development here, because we're not. SeL4 is designed for hard real time embedded systems and uses formal methods, which have and continue to be a mainstay approach in places which value security and reliability. And they really mean _reliability_ as in reliably wrong or reliably right.

So being able to adjust the spec and fix the system is actually a feature because it means your prover acts as a high-quality test.

As always, with systems like this if you use a formally-proven operating system kernel you will probably assess which other code paths in your application code are on the critical path and use formal methods on those components. And you will also be doing other less formal work like FMEA to complement. So you're not reliant on any one single method of assessing whether the system works, whether it meets the specification, and whether it can be relied upon to do the right thing in a bad situation.

  The systems we're talking about don't use SQL to communicate. They use data structures in a wire format of some sort because they are embedded systems. Don't pretend like we're talking about web development here, because we're not.

The other guy mentioned phones, which run UNIX clones. It is fairly obvious that we were talking about computing in general, which includes all of the things you claim to be out of scope.

  SeL4 is designed for hard real time embedded systems and uses formal methods, which have and continue to be a mainstay approach in places which value security and reliability.

Most embedded systems (e.g. the RP2040, the MSP430, etcetera) do not even have virtual memory protection, which makes seL4 a non option for them. When seL4 is an option, it is a tiny fraction of the code needed for the machine. All of that other code matters, especially since it is where the attack surface area is. seL4 on such machines is like the admin account in this picture; compromising what actually matters does not require compromising seL4:

https://xkcd.com/1200/

While seL4 is good at what it does, what seL4 does is extremely minimal and it is increasingly obvious that a vocal minority overrates it. Using seL4 is not going to stop vulnerabilities in userspace or even in drivers that were previously in kernel space, or in VMs running on top of it, but people who claim systems are insecure without seL4 insinuate that it will. They are like the Apple Store employee who once suggested to me that if I run Windows on Apple hardware, it will have none of the problems Windows normally has.

"process isolation is the bedrock of all other security guarantees" means process isolation is a necessary (in practice) condition, not a sufficient condition.

"Tell me how process isolation prevents SQL injection." is a non-sequitur because that is only coherent if they claimed process isolation is a sufficient condition.

To disagree with their position, you need to demonstrate a system where there is no process isolation and where maliciously crafted inputs intended to cause SQL injection can not result in undesired database access. So, one process gets to arbitrarily modify the contents of the SQL server process including changing the code and you need to prevent it from wrecking your database.

  "process isolation is the bedrock of all other security guarantees" means process isolation is a necessary (in practice) condition, not a sufficient condition

The attack surface of networked machines is unaffected by process isolation. It is only when you are already inside does process isolation have any use. Thus the idea that it is the bedrock is wrong.

  "Tell me how process isolation prevents SQL injection." is a non-sequitur because that is only coherent if they claimed process isolation is a sufficient condition.

It is a counter example that shows that process isolation is not the bedrock that it was claimed to be. Id sequitur.

  To disagree with their position, you need to demonstrate a system where there is no process isolation and where maliciously crafted inputs intended to cause SQL injection can not result in undesired database access. So, one process gets to arbitrarily modify the contents of the SQL server process including changing the code and you need to prevent it from wrecking your database.

Non sequitur applies here. The protection against SQL injection and process isolation have no link whatsoever. The fact that there is no link was my entire point. The example did not need to be SQL injection either. Telling me that I need to prove a link that is the opposite of what I was saying does not follow at all.

As I previously said, I could have cited just about any common vulnerability and process isolation would have done nothing about it. For example:

https://owasp.org/www-project-top-ten/

I only cited SQL injection because I could not think of any claim more absurd than the claim that process isolation is bedrock of guarantees against SQL injection, but if process isolation were the bedrock of all other security guarantees, then it would some relationship to protection against sql injection.

You do not appear to understand the difference between "necessary" and "sufficient".

Process isolation is not sufficient (i.e. adequate on its own) to make a SQL server secure against maliciously crafted inputs intended to cause SQL injection for the purpose of undesired database access because it does not sprinkle magical security pixie dust on it.

Process isolation is necessary (in practice) to make a SQL server secure against maliciously crafted inputs intended to cause SQL injection for the purpose of undesired database access because otherwise a attacker can just modify the code of the SQL server to directly do the undesired database accesses. Without process isolation your SQL server security/design can be bypassed.

The amazing thick walls of your castle do not matter if you built it on sand. The amazing solid bedrock is not sufficient to claim your castle is defensible if your castle is a wooden shack, but it is necessary for building a defensible castle.

A lack of process isolation does not allow your SQL server security to be bypassed when the adversary is not on the machine in the first place. The adversary would usually fill out a field on a form, which is where SQL injection attacks usually occur:

https://xkcd.com/327/

OSv for example does not have process isolation, yet applications on it are not considered insecure.

I read "bedrock" as 'necessary to all other security'. But arguing about word choice isn't useful; the question is what indolering actually meant.

"Tell me how process isolation prevents SQL injection."

You need process isolation to make the system secure enough to even require SQL injection. Otherwise, they can send packets to attack anything else on the system, get full privileges, and swap your SQL-enabled application with their own. While taking your database.

Further, techniques to block SQL injection work even better when they're in an isolated partition the attacker can't escape from. Even better if data can only flow in a specific way. Even better if it can be reliably cut off and recovered upon detection of a failure. That's why high-assurance guards used to sit between sensitive systems and untrusted networks. They did all of these things.

Now, for application-level issues. The Separation Kernel Protection Profile, which inspired designs like INTEGRITY-178B and seL4, called for secure middlewhere to protect communications between partitions or systems. That included message routers that enforced the security policy within the system. That would include protocol-level defenses, like for SQL requests, to protect communications outside the box.

seL4's isolation was, by itself, never intended to stop unrelated attacks. The vision, described in NICTA's Trustworthy Embedded Systems program, was to combine many components to do that. I'll add that seL4 team did a great job documenting the many points they may fail in their Assumptions page. They were much more open about it than most competing projects.

What? You'd put more faith in a kernel that has no formal verification of its conformance to a secure spec and has orders of magnitude more code in it that can go wrong? What is the basis for this confidence?

Does it even matter when the attack surface is in userspace? Formally verifying seL4 against a potentially buggy specification does not provide any assurances about the user space code that must run on top to produce a working system.

If you subscribe to the idea that the mere use of seL4 makes things more secure, you might use seL4 as a hypervisor beneath Linux on machines that would previously have run Linux on bare metal and then you would be using seL4, but you would not have made anything more secure. The increase in the TCB would suggest such a setup is less secure.

The security of a machine using seL4 is dependent on what runs on top of it because seL4 is not the boundary between attackers and their targets. The only exception would be if you are a virtual machine provider and then seL4 would only be part of the boundary, rather than the whole boundary.

> but you would not have made anything more secure.

This is does not follow. Why do you think a hypervisor with no verification to a spec is necessarily more secure than a hypervisor with a verification to a spec? Can you somehow quantify the latent bugs in the non-verified code?

The “that would previously have run Linux on bare metal” part of that sentence was important. Try reading it again. It never compared seL4 as a hypervisor to another hypervisor. It compared using seL4 as a hypervisor to not using a hypervisor at all on a machine that does not need a hypervisor. The addition of seL4 there is not only pointless, but possibly harmful if you consider the increased TCB size.

By the way, seL4 as a hypervisor uses components that are not verified to a specification, so saying that it is verified to a specification is not quite correct. They also seem to be proof of concept examples rather than a production solution when I look at their documentation:

https://docs.sel4.systems/projects/camkes-vm/

https://docs.sel4.systems/projects/camkes-vm/centos

Why is it that everyone on the “seL4 makes everything secure” bandwagon seems to have a tunnel vision that ignores that seL4 is useless without a large amount of unverified software that runs on top and that security will typically depend on that software, rather than seL4?

  What's odd about this argument is that such bugs would be at risk of reintroduction in any other piece of software.

They can be reintroduced into seL4 too. Just have an amendment to the specification adding a new feature say the bug is okay without anyone realizing it does.

  Sure, you get to score rhetorical points about the proof being incorrect once. But this bridge is now fixed and won't fail that way again in the same way.

The proof itself proved something other than what was advertised, which allowed for this issue to exist. If you look at the bug tracker, it appears that this has happened more than one time.

While seL4 is an amazing achievement, it is clear that it is not the bulletproof software that people thought it was. There is no proof that the specification is problem free after all.

  Cartels and governments regularly hack phones and spy on and even kill activists. The current processes you are defending get people killed and are undermining civil society.

This is a gross misrepresentation of what I said. Having an objective evidence based opinion that seL4 is not as good as advertised has nothing to do with people dying.

  SeL4 is a big deal and definitely worth the investments needed to make such reliability the norm instead of accepting the continual bridge collapses that occur in Linux land.

seL4 does not achieve this. It is the equivalent of less than 0.001% of all of the code run on machines. It makes no guarantees that the >99.999% that people use is okay.

> If you build a bridge to a specification and the bridge collapses, does saying that the specification was wrong in any way lessen the reality that the bridge failed?

You framed this as a loss of confidence in the techniques that prove the absence of various flaws. This bug should not undermine such confidence as the bug was always in the place (the spec) that would allow such bugs.

When seL4’s proof was published, people regarded seL4 to be flawless software and the fact that a problem in the specification would lead to issues was largely disregarded.

Now that it is clear that the specification has had problems, seL4 should not be considered issue free, since there is no proof that its specification is issue free and there is proof that its authors made a nonzero number of mistakes.

Anyone minimizing the impact of this flaw by saying “the specification was at fault here” completely misunderstands why the rest of the industry thought highly about these techniques in the first place. They had promised to produce flaw free software. Now that it is clear that is not true, the level of confidence the industry places in these techniques naturally needs to be adjusted. We cannot ignore the massive caveat of the specification needing to be flaw free anymore.

> When seL4’s proof was published, people regarded seL4 to be flawless software

No, that's not true. The framing was always that it surpassed an incredibly high safety bar that no other kernel had surmounted, far beyond even security certifications needed for protecting national secrets. This is still true.

> the level of confidence the industry places in these techniques naturally needs to be adjusted

No it doesn't, people using formal methods understand perfectly well what confidence verification should bring and the caveats that are necessary. If by "industry", you mean Joe-know-nothing-about-verification-shmoe, then I'm not sure why his opinion was particularly important to begin with.

the point are people not using formal methods yet. automotive for example continues amazing aspire iso 26262 rain dances to tell themselves systems were safe. and does not allow to replace that with formal specs and proofs of compliance. that's just complementary the "real safety work" has to be done with paperwork v model tracing.

  No, that's not true. The framing was always that it surpassed an incredibly high safety bar that no other kernel had surmounted, far beyond even security certifications needed for protecting national secrets. This is still true.

A number of people who read that interpreted it to mean seL4 is flawless. Now that flaws have been found, those people have had to re-evaluate their views. Those who understood seL4’s guarantees correctly are an extreme minority.

  No it doesn't, people using formal methods understand perfectly well what confidence verification should bring and the caveats that are necessary. If by "industry", you mean Joe-know-nothing-about-verification-shmoe, then I'm not sure why his opinion was particularly important to begin with.

>99.99% of the industry does not use formal methods, so those that understood the guarantees were weak enough to allow “impossible bugs” in the real world were an extreme minority. The rest of us had the view that I described.

You can deride people who do not do formal verification, but I guarantee everything you use has unverified code written by people who do not do formal verification. If we restricted computers to formally verified code, we would not have working computers, embedded or otherwise.

I do not see how that is a kernel memory corruption. I do not understand the code in context, but it appears to just be a case where the kernel incorrectly clobbered a userspace register which could result in incorrect userspace code execution. A error in that class would not inherently violate the system safety properties of the kernel itself.

If so, that would only fall under a functional specification problem in the userspace API making it hard to use the userspace API in the intended/desired way. That would make it hard to use the kernel and verify your system using the kernel, but it would not constitute a kernel memory corruption which is what safety specifications and proofs of the kernel itself would be concerned with.

I said that a memory corruption flaw was found in seL4. This is a fact. If you read the patch, you will see that a message that was just created had been being overwritten (which is explained in a code comment). This occurs inside the seL4 kernel code, and the proof previously permitted this behavior (according to one of the developers’ comments on the PR). The proof had to be amended to disallow this (which is the second PR). You should see this in the links.

You can not just assert it is a memory corruption without explaining how it is a memory corruption.

It appears to be a case where a wrong, but legal output is being stored. That does not, inherently, constitute a memory corruption.

For example, suppose I have a sorting function. I pass it a vector of integers by reference and I intend it modify it into a sorted vector of integers. Instead, that function zeros every element of my vector. That is a sorted vector, so it technically meets the specification. That function “corrupted” the contents of my vector. That is not a “memory corruption” bug. That is just a plain bug where I output the wrong thing into memory.

A memory corruption bug needs to violate the explicit or implicit invariants of the memory being “corrupted”. Out-of-bounds write, use-after-free, bypassing class interface, unguarded shared parallel access, etc. Writing incoherent, but legal values through provided pointers to uniquely owned memory is wrong, but not “memory corruption”.

Furthermore, this is not a definition game where we are disagreeing on the definition of “memory corruption”. They do not claim blanket safety from “memory corruption” which may be a class up to interpretation. They claim safety from [1]: buffer overflows, null pointer dereferences, pointer type confusion, memory leaks, and other specifically named and defined forms of memory corruption errors. Please identify which specific enumerated memory safety property was violated.

Again, I am not asserting it is not a memory corruption bug of some class. But it is very unclear from the patch and comments that the stated bug was actually a memory corruption without significantly more contextual detail. I literally do kernel development professionally and even I can not tell from the patch out-of-context; there is no way almost anybody else would be able to tell without more detail.

[1] https://sel4.systems/Info/FAQ/proof.html

See the FAQ entry on seL4 having zero bugs:

https://docs.sel4.systems/projects/sel4/frequently-asked-que...

Most who read that would expect the bug fixed in the linked GitHub PR to be impossible. The loophole was that the specification had a flaw, which was only mentioned as a vague hint about “unexpected features”.

You keep dancing around the question of it being a memory corruption despite confidently asserting it as a clear, indisputable fact. Please support your claim by identifying the specific memory safety property that was violated and how it was violated.

I provided citations. Use them and do your own research. I think you will find the answers in what the seL4 developers published, but I have no interest in spending days or even weeks pointing to things until you are satisfied.

You made a strong claim which you have failed to support adequately and yet have continued to double down on.

I did my research and presented my own interpretation which fundamentally disagrees with your interpretation. You have refused to address it, instead continuing to assert your interpretation without further detail. That does not prove my interpretation is correct, but it does indicate that the citations and evidence you have provided do not clearly lead to your conclusion and you neither identify the errors of my interpretation or directly demonstrate the correctness of your interpretation which could be done by demonstrating a simple counter-example demonstrating what memory is corrupted.

You claim it is indisputable fact, yet you claim it would take "days or even weeks" to present a clear example of the corruption. I do not see how you can claim the bug is clearly and indisputably a memory corruption bug that anybody can see from the citations you provided when it would take even you so long to provide a clear example.

I will say this. The seL4 developers made the strong claim. Evidence that it is not as strong as people who heard about it thought is not a strong claim. It is just being realistic. The seL4 developers themselves say that the properties they list are things that come out of the proof and your approach of looking for properties that they promise is a backward way of going about things, since they did not claim to exhaustively list all properties.

If you want to understand things to your satisfaction, read the proof and figure it out yourself. I have already understood things to my satisfaction and the double digit number of upvotes that I have received suggests to me that my explanation was to others’ satisfactions as well. You likely have many days or weeks or work ahead of you to answer a passing curiosity of yours whose precise answer is not going to change anything for anyone. Have fun.

that's not how that works.

writing into memory that doesn't belong to you is memory corruption. in this case: kernel (induced) memory corruption.

and it's really a bad thing:

functional safety technically boils down to the job of the kernel to provide "spatial and temporal freedom from interference", meaning all subsystems are isolated from each other. no "process" can write to another process, no process can starve another process. in this perspective, the kernel is another (special and privileged) process on the system.

a kernel that randomly writes to user space processes is inherently unsuitable for functional safety.

it's a huge no no. a failure in the goals and purpose of the kernel.

and finding this here specifically was heavily shaking up confidence in formal specifications and formal proofs of compliance to these specs.

Again, the nature of the bug has not been appropriately established. It appears to me to be a bug where a output register that the kernel is expected to write is written with a incorrect, but legal value in certain cases. If my interpretation is correct, which it might not be, that is just a wrong output not a "memory corruption". The claim of "memory corruption" needs a clear detailed explanation of what memory safety property is violated and how it violates that.

Second, no. The spatial separation guarantees you want from a kernel are that a domain can not induce spatial interference in a different domain that is isolated from the former. Internal memory corruption of a user domain, even uncontrolled asynchronous corruption by the kernel, makes it not very useful, but does not violate the protection property. This is a case where it is important to distinguish between "safety" and "usability". It is "safe", but not very "usable".

If your memory corruption only occurs during specified system calls, then that problem is further reduced making it easier to "use" the system. If the memory corruption is highly constrained, say it only corrupts in-bounds of passed in pointers, then it is easier to "use" once again. If there is no memory corruption, but it instead sometimes outputs invalid garbage, that is easier to "use" once again. If it outputs legal, but incorrect values, that is easier to "use" once again. None of these affect "system safety", but all are important bugs to fix to enable to creation of functional, usable systems.

fascinating. maybe terminology issues?

where I come from, the kernel must not, ever, write to unwanted locations, even if in theory it could.

wrong data as you point out is a completely different point of discussion, that could be a bug in the function which may or may not be safety critical , but hey, depending on the function you call, a wrong value could also come from some other process and the kernel is just the messenger of false data, not it's origin. no, "wrong value" that's not what I mean.

and a bug in the user process, writing data to the wrong place, also is not what I'm talking about.

what I consider violation of the functional safety requirement of spatial freedom form interference on the kernel is and unexpected "wrong location": the kernel "surprise surprise" writing to some address or some register (!) the kernel was not supposed to modify --- these _both_ are a violation of spatial freedom from interference, in the functional safety sense, to my limited understanding. "your dance area, my dance area" type of violations.

this reading comes from discussions about how if at all it might be possible to achieve this with a monolithic FOSS Linux kernel. There the page table can be set up to give quite some protections, even protecting user space from the kernel, but then who ensures the page tables aren't corrupted "somehow" by some rando kernel module? And similar discussions exist to reliably save and restore user space registers on context switches to the kernel...

but that's not what I wanted to get into, my point rather is: user space must be safe not only from other processes but also from the kernel. and that's something a microkernel can prove much easier than a monolith.

It is a nuanced point. Certainly, you want to have a API that conforms to specifications and does not ruin your desired program invariants. But what if it does? What if you make a specification error? How do you modularize your specification so errors in one part of the specification do not invalidate the rest?

For instance, suppose I have a kernel with spatial safety. I then add the system call, “Corrupt random memory in my own process at a random time”. Is that kernel still safe? All that function can do is destroy the invariants of the calling program. It can not turn a innocent isolated program malicious no matter how malicious another process is or became. What if nobody calls that function?

It would certainly be hard to use such a function for any purpose. It may allow a malicious input crafted by a communicating malicious process to cause a problem in a innocent, but incorrect program. But a correct, isolated program, using APIs correctly would be unaffected no matter what any program does even with access to that new “memory corruption on demand” API.

So, in this case, it would be fair and reasonable to classify the kernel as safe despite having a absurd system call in its specification. And, as basically any other API with a memory corruption is going to be less absurd, it only makes sense to classify those as “safe”, though very likely “unusable” or “hard to use”.

The distinction then becomes being able to cause memory corruption in isolated, correct programs. In that case, a program is no longer safe even if it proves itself correct. You must prove the entire system is correct and all other programs correct to establish any guarantees about any individual program. You can no longer “isolate” or “separate” your analysis which makes the problem even more intractable. That is the first problem you want to solve which is what this definition is intended to achieve.

a nuanced point indeed.

and we agree a kernel executing write_rando_stuff_to_rando_places out of the blue would be unsafe?

do we also agree registers to be auch random places?

then we're good

seL4 in Rust?

We should look at formal verification like everything else: in terms of statistical effectiveness. It's not really important whether or not there are _no_ bugs. What's important is how many bugs there are for each unit of "effort."

For example, if this were hypothetically the only bug that was ever found, then that would be a pretty damn good argument that formal verification is effective. Because the bug rate of other non-verified operating systems is much higher.

Has anyone added another formally proven layer or component? Yes, they're being added all the time. Recently added features:

- Support for a bunch of new architectures, including RISC-V. - Mixed criticality scheduling, which provides capability-based access to CPU time, mechanisms to limit the upper bound of execution of a thread, ensuring that high-criticality tasks have priority and access to necessary resources, and allowing "passive servers" which run on scheduling time donated by the caller. - Microkit, a new verified abstraction layer which made it much much easier to build actual systems using seL4. - Very recently, the Device Driver Framework, a device-driver template, control and data plane implementation, and tools for writing device drivers and providing device virtualisation for high-performance I/O on seL4.

Formal verification can guarantee that specific requirements hold in specific conditions. It's true that in general such requirements and conditions can be quite narrow. But seL4 itself has a whole lot of proofs about it, covering a wide range of properties that one would want in a kernel, and these guarantees hold under very weak assumptions. Even the correctness of the C compiler is not assumed, they have a separate tool which looks at the compiler output and proves that the compiled binary behaves correctly with respect to the required C semantics.

The requirements that seL4 meets include the following: the binary code of the seL4 kernel correctly implements the behaviour described in the abstract specification and nothing more. There are no buffer overflows, no memory leaks, no pointer errors or null pointer dereferences, no undefined behavior in the C code, no termination of the kernel apart from the explicit ways enumerated in the spec, etc. The specification and therefore the seL4 binary satisfy the security properties of integrity and confidentiality: the former means that there is absolutely no way for a process to change data that the process has no explicit permission to change, and the latter means that a process cannot, in any way, read data it has no explicit permission to read. It even shows that a process without permission cannot indirectly infer the data through certain side channels. Beyond security, the expected worst-case execution-time guarantees and scheduling properties are also met.

The developers of seL4 have been in funding hell for years. Most of their work was darpa research for remotely controlled drones. The US Military would very much like drones that can't be hacked.

Their current work is on LionsOS which is more towards greater adoptions: https://lionsos.org/

>The developers of seL4 have been in funding hell for years.

The actual story re: happenings in CSIRO is detailed in Gernot's blog[0], which is also quite interesting in its more technical posts.

0. https://microkerneldude.org/

For example: No buffer overflows, null pointer exceptions, use-after-free, etc. On ARM and RISCV64 not even the C compiler has to be trusted, because functional correctness has been proven for the binary. And there are more proofs besides functional correctness. https://docs.sel4.systems/projects/sel4/frequently-asked-que...

https://github.com/auxoncorp/ferros

Lots of type-level programming for tracking resources, hardware access, and capabilities at compile-time and trying to bring some of the underlying kernel guarantees up to the compiler because finding out about and debugging issues at runtime was just the absolute worst.

In high-assurance, formal methods were one of many used for the system. It was reduced complexity, precisely-specified behavior, likewise for security policy, proofs the design/code fulfilled it, exhaustive testing, leak analysis, pestering, and ability to recheck all this.

That's so hard it was mostly done for only kernels commercially. From there, your real-world use will involve user-level components, protocols with interactions, and so on. Add one thing to the proven TCB and maybe your proof disappears. So, every trusted component has to be rigorously designed. Then, all the interactions for a holistic argument.

Most don't do that. For example, seL4 hosting a web browser won't help you if it's a web application. IBOS and a WAF on seL4, all proven, might cover that. Harder argument. Most of these projects never go beyond the kernel or TLS stack or whatever.

You can do stuff with that. Look up Nizza Secure Systems Architecture for a paper with many examples. Yet, they usually don't cut it. They're not compatible with popular apps either. So, most people just harden Linux or BSD or Windows.

> IBOS and a WAF on seL4, all proven

If you mean web application firewall, that seems too complex to be proven? With infinite possible inputs, inspecting it would seem to require too much code to prove - unless it merely verifies traffic matches a short whitelist.

Why talk about high assurance talked in the past tense? Is the field moribund? (I don't mean to point out a typo, if that's what it is.)

It could potentially be proven. We think it's unlikely due to cost or complexity. So, the fields default position was that most things would be low to medium assurance. Only select components would be high assurance. I hope that answers your broader question about adoption of seL4-like techniques for larger systems.

Far as past tense, I left high-assurance security when I found out Jesus died for my sins and rose again. Had to learn an entirely new life with a focus on human beings instead of tech. I'm recently considering going back into security since I spend up to 12 hours a day at work anyway (two jobs).

I should also note another reason I say past tense. Many people I learned from have died, retired, or switched focuses. The reason for the later is that there's no real market for high-assurance security. Most won't spend the money or make the tradeoffs. So, security-enhancing popular platforms while assuming they'll get hacked (and responding correctly) seemed like a better use of time. I mean, I could probably could all the high-security vendors on my hands...

Congratuations on your big change, and on your courage. Security can help people, of course; it just depends on who you work for?

Thank you! And, yes, security can help people when your job allows you to do that. I was talking about high-assurance security specifically. That's products built with techniques like B3/A1 or EAL6/EAL7 required. Examples:

https://www.aesec.com/classic/DesigningTheGemsosSecurityKern...

https://lukemuehlhauser.com/wp-content/uploads/Karger-et-al-...

https://apps.dtic.mil/sti/pdfs/AD1014758.pdf

https://ghs.com/products/safety_critical/integrity_178_secur...

The market for this is tiny. NSA once estimated the labor force for developing them was under 200 people worldwide. I know maybe a dozen or so companies even selling such things. Given tough tradeoffs (eg less features), the buyer market is tiny even though development cost is higher.

Medium assurance is the best route commercially. That really just means a solid, development process with selective use of assurance-improving techniques. People writing key parts of their code in SPARK Ada or Rust with careful, design reviews is an example. Certain products, like HAProxy or OpenBSD, are coded so well they rarely have problems. Some web frameworks have security baked into them. Using such approaches is the most likely to succeed commercially. Others use architecture or hardware to great advantage, like Hydra Firewall or Secure64's SourceT.

The fields last idea for commercial high-assurance was "selfless acts of security" per Bell. He thought, one component or system type at a time, companies with the money should sponsor experts to build exemplars. They get maintained over time at hopefully lower cost. They're designed to be integrated into low-assurance systems to boost them. While using hybrid funding, CompCert, miTLS, and Muen SK are examples of this.

I just rarely see this happen. Both companies and FOSS favor ease of development or velocity over assurance of artifacts. The market usually requires integration with insecure systems whose integration itself might be impossible to secure. So, I have no optimism about high assurance but selective improvements are doable.

The document was updated in January.

A lot has happened in the last few years, such as the founding of seL4 foundation, the maturation of mixed criticality scheduling, the celebration of multiple seL4 summits, and the deployment in practical use by multiple companies and countries, in several scenarios.

Notably, Apple joined the seL4 foundation, as they use it in several of their products: https://sel4.systems/Foundation/Membership/ (Not sure if they've stated publicly which, but it's been pretty well known for a while now).

Reply on news.ycombinator.com