This was indeed a pleasant surprise when I logged into my CloudFlare account.
What intrigues me is that CloudFlare missed an opportunity to allow secure self-signed certificates.
The new CloudFlare SSL setup allows the origin server to present to CloudFlare's servers either (i) an unverified self-signed certificates; or (ii) a certificate signed by a CA. Neither provides great security. In the former case, a MITM can trivially generate a new self-signed certificate. History has shown the latter case is also problematic, as there have been several events where CAs have generated invalid keys [1].
What would be nice is if I could generate a self-signed certificate and upload the fingerprint(s) to CloudFlare. CloudFlare would could then verify the fingerprint when connecting to my origin server, without needing to trust a CA.
Am I missing anything obvious as to why this wouldn't be as secure (or more secure) than the two options CloudFlare has introduced?
> Maybe they have automatic theorem prover running on Jenkins and they just refuse to merge changes which would be proven to be wrong?
Yes, that's the plan.
Internally this is how we have been operating since 2009, when the proof was first completed: You don't push a change to the verified kernel branch unless you are willing (or are able to convince someone else) to do the proof updates.
We don't yet have a regression website publicly available, but it's on the short-term roadmap.
I'm not sure who submitted the link (I don't think it was anyone from the seL4 team), but I inserted the http://sel4.systems/ link into the repo's README file, which will hopefully help a little.
The seL4 kernel currently supports the ARMv6, ARMv7 and x86 architectures, though the proof only applies to ARMv6.
I am not sure what Genode's plans are. seL4 is a different kernel to OKL4, with a substantially different API, so it will be quite some work to move it across from OKL4 to seL4.
The prover has a bug (most proofs are done automatically).
Minor point: while many formal verification projects are proven automatically, seL4 is proven in Isabelle/HOL which is an interactive theorem prover. This means that the proofs are actually carried out mostly manually. (The downside is that it takes much longer to carry out proofs; the upside is that you can prove far more sophisticated properties than is possible with the current state-of-the-art automated provers).
You are still right that the proof checker could have a bug, though. Proof checkers tend to be much smaller and simpler than things like SMT solvers, which helps increase confidence in them, however.
INTEGRITY-178B and seL4 are not related in terms of their source code or origin, though they do both aim at the same target audience (security and/or safety-critical systems).
I don't have a good knowledge of INTEGRITY-178B, but as far as I can tell some differences are:
* INTEGRITY-178B is a static separation kernel. seL4 can be used as a static separation kernel, but also allows for dynamic systems, for instance with processes being created and torn-down dynamically at run-time;
* INTEGRITY-178B has a proof that a model of the code satisfies particular security properties, while seL4 has a proof that the actual C implementation satisfies particular properties;
* INTEGREITY-178B is certified to EAL6+, while seL4 has not undergone any external certification process. (Without having a good knowledge of EAL6+, my suspicion would be that the code-level aspects of seL4 would meet or exceed EAL6+ certification, while the process-level aspects would need work on the seL4 side.)
If someone has worked with INTEGRITY-178B, please correct me if I have made any mistakes.
Just a little bit more on this: NICTA was originally set up as a research group by the Australian Government with the explicit mandate of commercialising its research.
The OKL4 and seL4 microkernels developed by NICTA were commercialised through the company Open Kernel Labs, which was subsequently acquired by General Dynamics (who thus acquired the IP of both projects).
At NICTA, we are very happy to see seL4 finally being open sourced: we really do want to see our work be used as widely as possible, and open sourcing it is going to be the best way of this happening. (So, in response to the grandparent thread, that is why we are making a big fanfare: we are excited, even if nobody else is.)
The proof states that the C code of the kernel is a refinement of an high-level "abstract" specification of the kernel. This means that the C code only exhibits behaviours that are also exhibited by the high-level specification. The high-level specification (by construction) doesn't have certain bad behaviours that you often see in C programs: NULL pointer dereferences, buffer overruns, signed integer overflow, etc. Thus this class of bugs is proven to be absent. A good primer is available at: http://www.ertos.nicta.com.au/research/l4.verified/proof.pml
The original proof didn't make any claims about the high-level behaviour of the kernel, such as security. So for instance, the original kernel might have had a bug where you set up a system so that two processes shouldn't be able to communicate with each other, but after some unexpected sequence of API calls they form a communications channel between them.
NICTA in the following years after the initial proof carried out two security proofs: an integrity proof and an information flow proof. These proofs state that the capabilities possessed by a process determine (i) what other processes a particular process can modify; and (ii) what other processes the process can communicate with. Like the original proof, these security proofs (especially the second) have assumptions. In particular, they can only talk about parts of the system that are modelled. Timing channels, hidden CPU state, etc. not modelled by the proof may still allow information flow between processes, for instance.
Sorry, I don't think you can claim you have a mathematical proof of the correctness of your kernel when you assume this much.
You need to assume something. Every operating system kernel makes these assumptions: seL4 is just explicit about them. Some of the assumptions are bigger than others (management of caches is a pain to get right and hard to test, for instance). Some assumptions remain just due to a lack of time, such as proving the initialisation code of the kernel.
Additionally, as time has gone on the assumptions have been reduced. For instance, the work of Thomas Sewell and Magnus Myreen mean that the compiler no longer needs to be trusted: https://www.cl.cam.ac.uk/~mom22/pldi13.pdf
And where is this proof? I can't seem to find it anywhere on their web site.
The proof will be part of the open-source release. It consists of around 200,000 lines of Isabelle/HOL proof script, which is machine-checked. Anyone will be able to inspect/modify/check the proofs after the release.
I understand the word "must" to mean that they cannot add additional strings, such as payment, to their obligation to revoke the certificate. Is there another way of interpreting it that I am missing? I guess you could interpret it as "must provide a mechanism", but I can't see that that was the intent of the original document.
Mozilla's use of the word "must" here I think is important, because the barriers to correctly dealing with a security breach should be minimized. For better or worse, root CA's are entrusted with maintaining the security of large chunks of the internet. Charging users who suspect that their certificates _may_ have been compromised (due to the Heartbleed bug, in this case) will cause users to err on the side of inaction, which is going to weaken internet security in the long run.
"Visible on screen" unfortunately is a hard thing to determine. You can easily imagine a textbox with white text on a white background, or a very small textbox, or a textbox that briefly pops up whenever you type a keystroke or click the mouse, or...
Browsers really need to support some mechanism where the user can determine precisely what information will be filled prior to it being handed over to the website. This needn't be difficult; Chrome's existing autofill popup already displays a subset of the information, the popup just needs to give a fuller picture.
While you likely have a point that this is being sensationalised, the money analogy isn't quite accurate.
The problem is that such "evil" messages can be broadcast globally without the ability to remove them. A dollar bill with a message on it can be taken out of circulation; the bitcoin blockchain can't be reset without major chaos ensuing.
While such a scheme might solve this particular method of storing data, it won't make the general problem go away.
For instance, if I want to publish an 'n' byte message, I could generate 'n' wallets, each having as their final byte of their fingerprint the n'th byte of my message. Constructing 'n' such wallets will require on average "256*n/2" units of work---quite small, all things considered. I can then transfer a single bitcoin to each wallet in turn, forming a linked list of the bytes in my message. Even better, I also get my coin back at the end.
A few years back (6 months before the first Bing study in the article) Michael Kordahi developed a site "Blind Search" that anonymised search results from Google, Bing and Yahoo and put them side by side, letting users vote which they preferred.
The site (http://blindsearch.fejus.com/) now seems somewhat-defunct, with Yahoo results failing show. Aggregated results posted mid-2009 (http://delicategeniusblog.com/?p=839) (a little earlier than the original study) show Google on 41%, Bing 31%, Yahoo 28%, however.
As a purely non-scientific anecdote, I personally used the Blind Search website for a month mid-2011, preferring Google around 75% of the time, Yahoo 15% and Bing 10% of the time. (The latter two are interesting, because Yahoo is presumably using Bing's engine behind the scenes.) I probably don't represent a "typical user", however, as most of my queries are programming-related, which perhaps some search engines have better optimised for than others.
The original goal of the project was to have a verified computer stack, with proofs going from the software, compiler and processor all the way down to the gate level.
I am not sure how far they got, but I don't think the project is still active, which is a bit sad.
Edit: lower down in the fine print it states "per month", but the table heading states "p/message".