So if I find a bug or security bug does this speak to the usefulness of the formal verification claim?
Ironclad – formally verified, real-time capable, Unix-like OS kernel
81–90 of 151 posts
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#82Earlier quoted context omitted.
Is that an AI-generated page pretending to be a wiki?
Don't tell me you don't know this service. It's extremely useful to get to know the code and architecture of a project. You can even ask questions about the code and get the relevant references to the corresponding sections in the source files.
Okay but that's not a wiki. Wiki implies pages can be collaboratively edited and linked. Otherwise it's not a wiki, it's just a website. The only collaboration here is to bait people into becoming maintainers and fix the hallucinated content.
More than one maintainer has shown frustration at that site making up wrong documentation already.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#83Earlier quoted context omitted.
> why is this not used in conflicts to devastating effect? The systems with devastating impact are air-gapped. They're designed, audited, validated and then never touched again. Ports are disabled by cutting the traces on the motherboard and adding tamper protection to the case, which is in a secure facility protected by vetted people with guns, who are in a security facility protected by different vetted people with…
> The systems with devastating impact are air-gapped. You wish. More often than not the people building these think they are very clever by using their bullet proof fire walls rather than a physical disconnect. Or SLIP over a serial port because for some reason serial ports are fine. I've seen this kind of crap in practice in systems that should be airgapped, that they said were airgapped but that in fact were not ai…
If I had a dollar for each time I was told that they would get me a firewall exception to get to the air gapped system...
It does make it much easier to do stuff but kinda defeats the purpose.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#84Earlier quoted context omitted.
> why is this not used in conflicts to devastating effect? The systems with devastating impact are air-gapped. They're designed, audited, validated and then never touched again. Ports are disabled by cutting the traces on the motherboard and adding tamper protection to the case, which is in a secure facility protected by vetted people with guns, who are in a security facility protected by different vetted people with…
> The systems with devastating impact are air-gapped. You wish. More often than not the people building these think they are very clever by using their bullet proof fire walls rather than a physical disconnect. Or SLIP over a serial port because for some reason serial ports are fine. I've seen this kind of crap in practice in systems that should be airgapped, that they said were airgapped but that in fact were not ai…
While I can't talk to all the systems out there, I am talking about systems I have worked on.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#85Earlier quoted context omitted.
Don't tell me you don't know this service. It's extremely useful to get to know the code and architecture of a project. You can even ask questions about the code and get the relevant references to the corresponding sections in the source files.
Okay but that's not a wiki. Wiki implies pages can be collaboratively edited and linked. Otherwise it's not a wiki, it's just a website. The only collaboration here is to bait people into becoming maintainers and fix the hallucinated content. More than one maintainer has shown frustration at that site making up wrong documentation already.
It's just the name of the service, as imagined by its creator, Cognition Labs; it's called a "wiki" because it creates wiki-style documentation similar to Wikipedia's format. There are always people who complain about everything. I'm successfully using the service since a few month and even applied it to my own compiler projects, and I think it's pretty good; of course there are errors, but from my experience far less than the (mostly outdated, if available at all) design documentation you usually find for open-source projects.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#86Earlier quoted context omitted.
Any government can get RCE on any OS with the change in their couch. Formal verification of process isolation is REALLY important when lives depend on it. That's a huge value add! My main concern is speed and the lack of capability based security. seL4 is faster than Linux by a mile and I'm guessing that this is much slower. You can put a POSIX layer on seL4 but POSIX is inherently flawed too. MAC separates privilege…
> Any government can get RCE on any OS with the change in their couch. Do you really believe that? That seems extremely implausible based on just simple observations like all governments using COTS OS for military/intelligence work or standard OS:es being used for critical infrastructure like power/water/finance/transportation. If your statement was even remotely true then why is this not used in conflicts to devasta…
> Do you really believe that? That seems extremely implausible based on just simple observations like all governments using COTS OS for military/intelligence work or standard OS:es being used for critical infrastructure like power/water/finance/transportation.
I do, but have a slightly different take: even though COTS software is pretty much unilaterally full of bugs that will be exploitable and could be found, it is still possible to compose layers of security that compliment each other in such a way that a compromise in any one layer wouldn't mean game over. Done very carefully, I think you can make a stack vastly more secure than the sum of its parts. Moreover, it's very possible to make exploiting the software both more annoying and easier to detect, which would dissuade attempting to use exploits.
> If your statement was even remotely true then why is this not used in conflicts to devastating effect?
I think the costs, risks and incentives need to line up properly to actually see things play out. Even though software exploits in COTS software is relatively cheap by government money standards, they do still take time and money. Not to mention the actual software exploit part may not even be the most expensive or complicated part of an operation, especially if you desperately need to evade detection for a long time, and especially if your adversary is going to have sufficient auditing to know something is wrong early.
Stuxnet is old, but surely one of the most fascinating uses of malware in geopolitics. But wow, the amount of work involved and knowledge needed to make something like that happen makes the exploit part feel rather small.
Formally verified software seems to have a lot of promise, then, to make deep exploits even more convoluted, expensive and rare. Surely there will still be bugs, but it leaves a lot less room for error, and very well could shift the calculus on security threats a bit.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#87Interesting. Ada is in the greater Wirthian family (it's Pascal-like), and until now, the only Unix-like kernel I was aware of in a Wirthian language was TUNIS:
https://en.wikipedia.org/wiki/TUNIS
It was implemented in Concurrent Euclid.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#88Earlier quoted context omitted.
> The systems with devastating impact are air-gapped. You wish. More often than not the people building these think they are very clever by using their bullet proof fire walls rather than a physical disconnect. Or SLIP over a serial port because for some reason serial ports are fine. I've seen this kind of crap in practice in systems that should be airgapped, that they said were airgapped but that in fact were not ai…
If I had a dollar for each time I was told that they would get me a firewall exception to get to the air gapped system... It does make it much easier to do stuff but kinda defeats the purpose.
And a firewall is not an airgap.
And a WiFi connection even though it goes 'through the air' is not an airgap.
The same for BT and any other kind of connectivity.
An airgap is only an airgap if you need physical access to a device to be able to import or export bits using a physical connection, and the location of the device is secured by physical barriers. Preferably a building that is secure against non-military wannabe intruders.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#89Interesting. Ada is in the greater Wirthian family (it's Pascal-like), and until now, the only Unix-like kernel I was aware of in a Wirthian language was TUNIS: https://en.wikipedia.org/wiki/TUNIS It was implemented in Concurrent Euclid. https://en.wikipedia.org/wiki/Concurrent_Euclid
> the only Unix-like kernel I was aware of in a Wirthian language was TUNIS
SPIN developed at the University of Washington in the nineties was written in Modula-3; it was a microkernel-based system and supported the Digital UNIX system call interface, allowing Unix applications to run. There was also Sol implemented at INRIA in a Pascal dialect in the eighties which offered a Unix-compatible environment; it was followed by Chorus (initially written in Pascal), also a microkernel-based system, compatible with Unix APIs.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#90(partially) formally verified says right on the page
https://ironclad-os.org/formalverification.html