[cryptography] seL4 going open source
http://sel4.systems/ General Dynamics C4 Systems and NICTA are pleased to announce the open sourcing of seL4, the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement. It is still the world's most highly-assured OS. What's being released? It will include all of the kernel's source code, all the proofs, plus other code and proofs useful for building highly trustworthy systems. All will be under standard open-source licensing terms. More details will be posted here closer to the release date. When is it happening? The release will happen at noon of Tuesday, 29 July 2014 AEST (UTC+10), in celebration of International Proof Day (the fifth aniversary of the completion of seL4's functional correctness proof). ... http://sel4.systems/About/ What's special about seL4? Completely unique about seL4 is its unprecedented degree of assurance, achieved through formal verification. Specifically, the ARM version of seL4 is the first (and still only) general-purpose OS kernel with a full functional correctness proof, meaning a mathematical proof that the implementation (written in C) adheres to its specification. In short, the implementation is proved to be bug-free. This implies a number of other properties, such as freedom from buffer overflows, null pointer exceptions, use-after-free, etc. There is a further proof that the binary code that executes on the hardware is a correct translation of the C code. This means that the compiler does not have to be trusted, and extends the functional correctness property to the binary. Furthermore, there are proofs that seL4's specifcation, if used properly, will enforce integrity and confidentiality, core security properties. Combined with the proofs mentioned above, these properties are guaranteed to be enforced not only by a model of the kernel (the spec) but the actual binary. Therefore, seL4 is the world's first (and still only) OS that is proved secure in a very strong sense. Finally, seL4 is the first (and still only) protected-mode OS kernel with a sound and complete timeliness analysis. Among others this means that it has provable upper bounds on interrupt latencies (as well as latencies of any other kernel operations). It is therefore the only kernel with memory protection that can give you hard real-time guarantees. ... ___ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography
Re: [cryptography] seL4 going open source
On 6/24/2014 1:43 PM, ianG wrote: http://sel4.systems/ General Dynamics C4 Systems and NICTA are pleased to announce the open sourcing of seL4, the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement. It is still the world's most highly-assured OS. What's being released? It will include all of the kernel's source code, all the proofs, plus other code and proofs useful for building highly trustworthy systems. All will be under standard open-source licensing terms. More details will be posted here closer to the release date. When is it happening? The release will happen at noon of Tuesday, 29 July 2014 AEST (UTC+10), in celebration of International Proof Day (the fifth aniversary of the completion of seL4's functional correctness proof). ... http://sel4.systems/About/ What's special about seL4? Completely unique about seL4 is its unprecedented degree of assurance, achieved through formal verification. Specifically, the ARM version of seL4 is the first (and still only) general-purpose OS kernel with a full functional correctness proof, meaning a mathematical proof that the implementation (written in C) adheres to its specification. In short, the implementation is proved to be bug-free. This implies a number of other properties, such as freedom from buffer overflows, null pointer exceptions, use-after-free, etc. There is a further proof that the binary code that executes on the hardware is a correct translation of the C code. This means that the compiler does not have to be trusted, and extends the functional correctness property to the binary. Furthermore, there are proofs that seL4's specifcation, if used properly, will enforce integrity and confidentiality, core security properties. Combined with the proofs mentioned above, these properties are guaranteed to be enforced not only by a model of the kernel (the spec) but the actual binary. Therefore, seL4 is the world's first (and still only) OS that is proved secure in a very strong sense. Finally, seL4 is the first (and still only) protected-mode OS kernel with a sound and complete timeliness analysis. Among others this means that it has provable upper bounds on interrupt latencies (as well as latencies of any other kernel operations). It is therefore the only kernel with memory protection that can give you hard real-time guarantees. ... ___ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography I think this is great! -- Kevin ___ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography
[cryptography] List of digital currencies?
Any links to a list of digital currencies organized by technology? ie: Bitcoin has countless forks characterized by nothing more than adjusting (or not) the operating parameters of the bitcoin.org code and starting their own genesis. Others may swap out the hash or crypto functions within that. While useful to list them all under the aforesaid parent technology 'Bitcoin', they are all ultimately uninteresting and a waste of time to research. A real list would group all the digital currencies by genuine differences in architecture... those archs thus resulting in their suitability to different applications, capabilities to anonymity, features for centralization/regulation, etc. So now you might have Bitcoin Paypal, Linden Some other various coin designs Currencies that pass serialized 'banknotes' around ___ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography
Re: [cryptography] How big a speedup through storage?
Date: Sat, 21 Jun 2014 03:10:58 -0400 From: grarpamp grarp...@gmail.com To: Crypto discussion list cryptography@randombit.net Cc: cypherpu...@cpunks.org, cryptography cryptogra...@metzdowd.com Subject: Re: [cryptography] How big a speedup through storage? Message-ID: cad2ti2_dcrqrnp30qjjdoh95zcf2e7qh1nw_lrn9v-0nv5o...@mail.gmail.com Content-Type: text/plain; charset=UTF-8 [...] I meant as answer 'estimates on how big' question. Take what we know about storage, figure in some good efficiencies for the 'storage only' case. And figure what can be bought and operated year on year per foot. You could hide/support $1B + $1B/year but $10B/yr would be hard given entire intel budget is $80B, or $50+B if you drop mil. So... 1) How big can you get within budget? 2) What can you do with it re: a) crypto, or b) otherwise? https://en.wikipedia.org/wiki/United_States_intelligence_budget https://en.wikipedia.org/wiki/United_States_Intelligence_Community http://www.martingrandjean.ch/data-visualization-top-secret-us-intelligence-budget/ In re the Bluffdale facility, it has about 100,000 square feet of actual data warehouse, and is equipped to support a 65 megawatt power demand and uses 1.7 million gallons of water per day for cooling. This gives a baseline for estimating the power density and processing capacity of the largest (known) U.S. TLA data center. An open question: Is all that space for long term storage enabling retroactive surveillance of future enemies of the State, or is some portion of its capacity dedicated to cryptography? http://www.wired.com/2012/03/ff_nsadatacenter/all/1 ___ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography
Re: [cryptography] List of digital currencies?
On Tue, Jun 24, 2014 at 1:02 PM, grarpamp grarp...@gmail.com wrote: Any links to a list of digital currencies organized by technology? ie: Bitcoin has countless forks characterized by nothing more than adjusting (or not) the operating parameters of the bitcoin.org code and starting their own genesis. Others may swap out the hash or crypto functions within that. While useful to list them all under the aforesaid parent technology 'Bitcoin', they are all ultimately uninteresting and a waste of time to research. agreed. but have you seen the majesty of my wuffie? ___ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography
