Open fproulx-pbox opened 10 years ago
I see, how was the parser developed? Was it generated using a parser generator with formal proof? I consider parsing as area to always handle carefully
OK. So considering you do not use browser native functions, the security of CCM and RSA padding may be affected by weak random or nonce reuse when you provide IV from the outside ? For instance, SJCL uses window.crypto.getRandomValues() how should we safely provide randomness while keeping your assumptions true.
Le 05/06/2014 20:05, François Proulx a écrit :
I see, how was the parser developed? Was it generated using a parser generator with formal proof? I considering parsing always an area to be careful handled with...
That's an excellent consideration, parsing is often security critical and easy to do wrong. But the answer to your question is no - this parser is NOT generated from a formally verified parser generator. It is manually written and I cannot guarantee that it doesn't have bugs - however, that's not the goal of this library, and none of the cryptographic functions carry proof of their functional correctness either. This will hopefully change in the future - adding support for verified parsing is one of the goals of the F* project https://github.com/FStarLang/FStar (eventually,the whole DJCL is meant to be generated from verified F*)
OK. So considering you do not use browser native functions, the security of CCM and RSA padding may be affected by weak random or nonce reuse when you provide IV from the outside ? For instance, SJCL uses window.crypto.getRandomValues() how should we safely provide randomness while keeping your assumptions true.
It is not a problem in itself - you must supply the IVs and nonces to the cryptographic primitives. If you are writing a fully wrapped defensive function, the server that loads the script must inject enough entropy for the IVs that will be required (if you are running out, you can do encrypted CORS to get more). Read the "Script Server" tab on defensivejs.com for details.
DJCL is written in DJS, a subset of JavaScript that doesn't allow the use any DOM or external function because they can be tampered. See http://www.defensivejs.com for details and motivations