Add audit docs

README.md

@@ -2,18 +2,23 @@
 
 Jess is a cryptographic library and cli tool that focuses on usability and freedom.
 
-DISCLAIMER: This is still work in progress. Breaking changes might still occur. Do _not_ use in production yet! Use at your own risk.
+__Project Status__:
+- Core Logic: production & [audited](docs/AUDITS.md)
+- Go API: non-final production (breaking changes might happen)
+- CLI Tool: working alpha stage, rough around the edges
+
+DISCLAIMER: Do _not_ use in production yet! Use at your own risk.
 
 ### Usage & Intro
 
 Jess uses the theme of envelopes and letters in order to make everything a bit more comprehensible. Here is a list of terms that will prove helpful:
-- __Signet__ private or secret key
-- __Recipient__ public key
-- __Envelope__ encryption configuration
-- __Letter__ encrypted data with associated configuration
-- __Trust Store__ a storage of everything you trust, your own keys and configurations, and your friends' public keys.
+- __Signet__ ... private or secret key
+- __Recipient__ ... public key
+- __Envelope__ ... encryption configuration
+- __Letter__ ... encrypted data with associated configuration
+- __Trust Store__ ... a storage of everything you trust, your own keys and configurations, and your friends' public keys.
 
-Jess makes heavy use of `trust stores`, which in its basic form is just a directory, where you can store your keys and configuration. You can either set a default through an environment variable, or set it manually every time. This makes it easy to compartmentalize your trust zones.
+Jess makes heavy use of `trust stores`, which in its basic form is just a directory, where you can store your keys and configuration. You can either set a default one through an environment variable, or set it manually every time. This makes it easy to compartmentalize your trust zones.
 
 Here is how you can setup a trust store and generate some keys:
 
@@ -46,8 +51,8 @@ Normally, of course, you would have a friend send you their `recipient` file (pu
 In order to help you not screw up any configuration, Jess has the concept of __requirements__:
 - Confidentiality ... hide contents
 - Integrity ... check that nothing was modified
-- Recipient Authentication ... verify identity of recipient
-- Sender Authentication ... verify identity of sender
+- Recipient Authentication ... verify recipient
+- Sender Authentication ... verify sender
 
 By default, all of them are required. If you, for some reason, do not require one ore more of them, you will have to disable them in the envelope for closing an envelope (encrypting) and pass the reduced requirements when opening a letter (decrypting).
 

docs/AUDITS.md

@@ -0,0 +1,33 @@
+# Audits
+
+## Audit #001
+
+In January 2020, the project was audited by [Cure53](https://cure53.de/).  
+Cure53 was chosen because they have proven to both excell as auditors as well as being committed to building a more open and better Internet - I mean, just have a look at their [publications](https://cure53.de/#publications)!
+
+[This commit](https://github.com/safing/jess/commit/648d16d1cc8185ed3704373e43c84a6ab4315498) was handed in for the audit.  
+Fixes can be found in [PR #3](https://github.com/safing/jess/pull/3) and was merged [here](https://github.com/safing/jess/commit/41fbc87f119a7d69f0fd9f24275e245fd4e2eedf).
+
+They found 5 issues:
+
+__Secure key deletion ineffective (Medium Severity)__  
+Golang does not yet provide a secure way of handling key material. The is no clean fix, we were advised to wait. Documentation has been updated to reflect this.  
+See [Github issue](https://github.com/golang/go/issues/21865) for details.
+
+__Password KDF vulnerable to GPU/ASIC attacks (Medium Severity)__  
+PBKDF2 is vulnarable to GPU/ASIC attacks, was replaced with scrypt with a much higher security margin (rounds).
+
+__Secure channel protocol weaknesses (High Severity)__  
+Verification of the protocol with [Verifpal](https://verifpal.com) revealed that in addition to one expected weakness, there is another. The found weakness should actually have been expected, because it is a limitation of the protocol. The main use case of the protocol, securing SPN connections, is not impacted. Documentation was updated.
+
+__Key management/encryption with 1-byte key (Critical Severity)__  
+This was just a devops error. We forgot to replace a "FIXME" comment with a function call. 🙈
+
+__Unnecessary configurability considered dangerous (Medium Severity)__  
+This was somewhat expected. We did not yet know how to best expose the configurability to users. We were advised: NOT. We implemented changes and introduced cipher suites that specify a fixed sets of algorithms and security guarantees.
+
+The full report is available [in-repo here](audit_001_report_cure53_SAF-01.pdf) or [directly from the auditor](https://cure53.de/pentest-report_safing-jess.pdf).
+
+# Formal Verification
+
+In the first Audit by Cure53, one of the auditors, [Nadim Kobeissi](https://nadim.computer/), used his software [Verifpal](https://verifpal.com/) for an automated formal verficiation of the wire protocol. This was quite an amazing thing, as we wrote the model definition _in_ the kickoff meeting. Verifpal then combed through the model to check if it really holds up to its promises. You can find the model [here](key_establishment_dh.vp).

docs/key_establishment_dh.vp

@@ -0,0 +1,51 @@
+attacker[active]
+
+principal Client[
+	generates e1
+	ge1 = G^e1
+]
+
+principal Server[
+	knows private s
+	generates se
+	gse = G^se
+	gs = G^s
+	gseSignature = SIGN(s, gse)
+]
+
+Server -> Client: [gs], gse, gseSignature
+
+principal Client[
+	_ = SIGNVERIF(gs, gse, gseSignature)?
+	knows private msg1
+	s1c = gse^e1
+	enc1 = AEAD_ENC(s1c, msg1, HASH(gs, gse, ge1))
+]
+
+Client -> Server: ge1, enc1
+
+principal Server[
+	s1s = ge1^se
+	dec1 = AEAD_DEC(s1s, enc1, HASH(gs, gse, ge1))?
+	generates e2
+	s2s = ge1^e2
+	ge2 = G^e2
+	s3s = HKDF(s1s, s2s, nil)
+	knows private msg2
+	enc2 = AEAD_ENC(s3s, msg2, HASH(gs, gse, ge1, ge2))
+]
+
+Server -> Client: ge2, enc2
+
+principal Client[
+	s2c = ge2^e1
+	s3c = HKDF(s1c, s2c, nil)
+	dec2 = AEAD_DEC(s3c, enc2, HASH(gs, gse, ge1, ge2))?
+]
+
+queries[
+	confidentiality? msg1
+	confidentiality? msg2
+	authentication? Client -> Server: enc1
+	authentication? Server -> Client: enc2 
+]