Re: [rust-dev] Cryptol, the language of cryptography
On Sun, Apr 27, 2014 at 1:48 AM, Daniel Micay danielmi...@gmail.com wrote: On 26/04/14 05:42 PM, Gregory Maxwell wrote: One of the things that is less hopeless and may inform the language spec (and library) is writing code that can keep all data structures that keep secret keys in mlocked and zeroed-after-use memory that comes along with doing crypto but which aren't the crypto themselves. You should really just be doing it in another process at that point. Unfortunately, that's not a common solution, look at most webservers right now... So, because fixing timing leaks is very hard in reduced cases and impossible to do in the general case, it means that we should not even try? Do I have to worry about power analysis on a server? Can I write assembly myself to make sure the compiler will not optimize stuff away? The current solutions are not pretty and do not solve everything, but they reduce the risk. ___ Rust-dev mailing list Rust-dev@mozilla.org https://mail.mozilla.org/listinfo/rust-dev
Re: [rust-dev] Cryptol, the language of cryptography
There is nothing hard about it, assuming you are using a decent language. Just add a CryptoT type that wraps integers and booleans and that doesn't allow any non-constant time operations nor implicit conversion to anything that is not CryptoT (which of course means you can't index memory or do branches based on it). If the optimizer can screw up things, implement the CryptoT operations in assembly. ___ Rust-dev mailing list Rust-dev@mozilla.org https://mail.mozilla.org/listinfo/rust-dev
Re: [rust-dev] Cryptol, the language of cryptography
On Sat, Apr 26, 2014 at 3:26 AM, John Mija jon...@proinbox.com wrote: In summary, Cryptol helps to implement existing known crypto algorithms correctly, but also to design new crypto algorithms. Cryptol isn't some kind of magic silver bullet for implementing crypto correctly. While it can help keep crypto implementations closer to their mathematical descriptions, and help formally verify them, that's only half the battle. So, please review the inclusion of crypto. library in the standard lib. As far as I'm concerned, Cryptol changes nothing when it comes to including crypto in Rust's standard library. For starters, Cryptol seems to be something of a self-contained crypto ecosystem, and it's not clear at least to me how it can be applied to verifying crypto implementations in other languages. Even if it could, crypto implementations still need to be verified by security auditors, preferably by multiple, independent auditors. Having crypto in the standard library limits agility around shipping security updates, since now you must update the entire standard library, and not just one library. -- Tony Arcieri ___ Rust-dev mailing list Rust-dev@mozilla.org https://mail.mozilla.org/listinfo/rust-dev
[rust-dev] Cryptol, the language of cryptography
The cryptography library was removed from the standard library because there was not way to verify the possible issues in the algorithms implementations. But luckly, there is already a DSL designed for such task: http://cryptol.net/index.html https://news.ycombinator.com/item?id=7642434 http://2012.sharcs.org/slides/hurd.pdf In summary, Cryptol helps to implement existing known crypto algorithms correctly, but also to design new crypto algorithms. So, please review the inclusion of crypto. library in the standard lib. ___ Rust-dev mailing list Rust-dev@mozilla.org https://mail.mozilla.org/listinfo/rust-dev
Re: [rust-dev] Cryptol, the language of cryptography
I think the bigger issue is that we really need someone who lives and breathes cryptography before we feel okay about shipping crypto code. Bugs with crypto don't often happen because of poorly implemented primitives: they happen when you combine those primitives in bad ways. Formal analysis doesn't help there. ___ Rust-dev mailing list Rust-dev@mozilla.org https://mail.mozilla.org/listinfo/rust-dev
Re: [rust-dev] Cryptol, the language of cryptography
On Sat, Apr 26, 2014 at 3:21 PM, Steve Klabnik st...@steveklabnik.comwrote: I think the bigger issue is that we really need someone who lives and breathes cryptography before we feel okay about shipping crypto code. Bugs with crypto don't often happen because of poorly implemented primitives: they happen when you combine those primitives in bad ways. Formal analysis doesn't help there. Before writing production ready crypto code, some things must be tested carefully, like the ability to write constant time code, or a secure buffer implementation (wiped before freeing it). Constant time code is possible in theory (the Rust-crypto has an AES implementation with precautions for that), but I do not know what could be messed up by LLVM optimizations there. Still, with the possibility of dropping some assembly directly where it is needed, it is a great platform for crypto experimentation. ___ Rust-dev mailing list Rust-dev@mozilla.org https://mail.mozilla.org/listinfo/rust-dev
Re: [rust-dev] Cryptol, the language of cryptography
On 26 Apr 2014, at 18:39, Geoffroy Couprie geo.coup...@gmail.com wrote: Constant time code is possible in theory As long as you don’t do memory accesses, branches, division, floating-point, etc. Some x86 processors even have variable-time multiplication. Writing constant-time code is essentially impossible.___ Rust-dev mailing list Rust-dev@mozilla.org https://mail.mozilla.org/listinfo/rust-dev
Re: [rust-dev] Cryptol, the language of cryptography
On Sat, Apr 26, 2014 at 6:55 PM, Jens Nockert j...@nockert.se wrote: On 26 Apr 2014, at 18:39, Geoffroy Couprie geo.coup...@gmail.com wrote: Constant time code is possible in theory As long as you don’t do memory accesses, branches, division, floating-point, etc. Some x86 processors even have variable-time multiplication. Writing constant-time code is essentially impossible. Like most software problems, they're hard in the general case, but doable in specific cases. Yes, that requires taking into account cache lines, counting CPU cycles for every instruction, making sure you do not branch depending on secret information, be wary of concurrent use of the processor, and adapt all of that to the specific processor you target. Yet it has been done for some algorithms and processors. It is insanely hard, few are able to do it correctly, but it is still a worthwhile target. ___ Rust-dev mailing list Rust-dev@mozilla.org https://mail.mozilla.org/listinfo/rust-dev
Re: [rust-dev] Cryptol, the language of cryptography
* Steve Klabnik: Bugs with crypto don't often happen because of poorly implemented primitives: they happen when you combine those primitives in bad ways. Formal analysis doesn't help there. That's exactly where formal analysis does help. However, real-world protocols are quite difficult to model, and programmers expect interfaces which make parts of the application part of the model. ___ Rust-dev mailing list Rust-dev@mozilla.org https://mail.mozilla.org/listinfo/rust-dev
Re: [rust-dev] Cryptol, the language of cryptography
On 26/04/14 01:04 PM, Geoffroy Couprie wrote: counting CPU cycles for every instruction This isn't possible. A modern CPU has a long pipeline and the OS is also doing preemptive context switches. signature.asc Description: OpenPGP digital signature ___ Rust-dev mailing list Rust-dev@mozilla.org https://mail.mozilla.org/listinfo/rust-dev
Re: [rust-dev] Cryptol, the language of cryptography
On Sat, Apr 26, 2014 at 9:39 AM, Geoffroy Couprie geo.coup...@gmail.com wrote: Before writing production ready crypto code, some things must be tested carefully, like the ability to write constant time code, or a secure buffer implementation (wiped before freeing it). Constant time code is possible in theory (the Rust-crypto has an AES implementation with precautions for that), but I do not know what could be messed up by LLVM optimizations there. Still, with the possibility of dropping some assembly directly where it is needed, it is a great platform for crypto experimentation. Even in plain C it is very hard to make any guarantees from the source code level. The C abstract machine doesn't promise how much time things take and the compiler is free to make optimizations that change the timing, though at the moment doing 'the obvious thing' for constant timeness seems to mostly not get broken by the optimizer there really are no promises, and an upgraded toolchain could change the behavior— which is especially bad because its difficult to construct reliable tests for constant-timeness. And all this before you start worrying about how the cpu pipeline might leak timing information even if all the instructions are supposed to be constant time, or the leakage from power analysis which seem impossible to close without specially constructed hardware. One of the things that is less hopeless and may inform the language spec (and library) is writing code that can keep all data structures that keep secret keys in mlocked and zeroed-after-use memory that comes along with doing crypto but which aren't the crypto themselves. ___ Rust-dev mailing list Rust-dev@mozilla.org https://mail.mozilla.org/listinfo/rust-dev
Re: [rust-dev] Cryptol, the language of cryptography
On 26/04/14 05:42 PM, Gregory Maxwell wrote: One of the things that is less hopeless and may inform the language spec (and library) is writing code that can keep all data structures that keep secret keys in mlocked and zeroed-after-use memory that comes along with doing crypto but which aren't the crypto themselves. You should really just be doing it in another process at that point. signature.asc Description: OpenPGP digital signature ___ Rust-dev mailing list Rust-dev@mozilla.org https://mail.mozilla.org/listinfo/rust-dev
