Viewing profile — daveasdf

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 "…

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. T…

> 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 …

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…

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…

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…

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 do…

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…

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 exhi…

> 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 anoth…

"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 b…

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…

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 g…

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 an…

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, w…