daveasdf

6 ms·

1.
by daveasdf 12y ago
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".
2.
by daveasdf 12y ago
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 pres
3.
by daveasdf 12y ago
> 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 wa
4.
by daveasdf 12y ago
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.
5.
by daveasdf 12y ago
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 wil
6.
by daveasdf 12y ago
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 proo
7.
by daveasdf 12y ago
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 a
8.
by daveasdf 12y ago
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 th
9.
by daveasdf 12y ago
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 by the
10.
by daveasdf 12y ago
> 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 missing? I
11.
Public Consultation on the review of the EU copyright rules(ec.europa.eu)
1 points by daveasdf 13y ago|0 comments
12.
by daveasdf 13y ago
"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 cl
13.
by daveasdf 13y ago
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
14.
by daveasdf 13y ago
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 thei
15.
by daveasdf 14y ago
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
16.
by daveasdf 14y ago
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 prefe
17.
by daveasdf 15y ago
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, compiler and processor