Now the pricing page states "(p/message)". Was this a typo, or is it really $5 per message? Edit: lower down in the fine print it states "per month", but the table heading states "p/message".
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…
> 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…
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…
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…
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…
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…
This reeks of bull shit 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…
> CAs must revoke [...] 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…
"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…
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…
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…
I am not seeing it from here. (Australia, GMT+10 time-zone). However it is available from the Google doodle archives at: http://www.google.com/doodles/douglas-adams-61st-birthday
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…
You might be thinking of Verisoft and their "VAMP" hardware stack: http://www.verisoft.de/SubProject2.html The original goal of the project was to have a verified computer stack, with proofs going from the software,…
Now the pricing page states "(p/message)". Was this a typo, or is it really $5 per message? Edit: lower down in the fine print it states "per month", but the table heading states "p/message".
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…
> 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…
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…
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…
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…
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…
This reeks of bull shit 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…
> CAs must revoke [...] 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…
"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…
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…
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…
I am not seeing it from here. (Australia, GMT+10 time-zone). However it is available from the Google doodle archives at: http://www.google.com/doodles/douglas-adams-61st-birthday
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…
You might be thinking of Verisoft and their "VAMP" hardware stack: http://www.verisoft.de/SubProject2.html The original goal of the project was to have a verified computer stack, with proofs going from the software,…