make security properties of block cypher etc. evident in types

[dckc]

I found the Probabilistic relational verification types work in the F* project very interesting:

Recall that non-interference means that public results do not
depend on secrets. If an expression e with base type a that computes
over some secret information can be given the type

type eq a = x:a{|L x = R x|}

then its result can be safely published, since the execution of e
reveals no information about the secrets.
...
In cryptography, confidentiality is usually stated
as resistance against chosen-plaintext attacks (CPA) ... Instead of reasoning about
two messages selected by b, we just need to show that the function
let cpa’ p = encrypt (sample n) p has the type block → eq block .

I'm not quite sure how well F* effects translate to idris effects, but it seems to me that it's essential to represent these security properties in the types, and not just the number of bits and bytes in the input and output parameters.

All this type tells me is that the function goes from some number of bits to bits; it doesn't express any actual security properties:

encryptBlock : k -> Bits bitsPerBlock -> Bits bitsPerBlock

The identity function satisfies that type, as do constant functions, etc.

[sellout]

Thanks for that paper. I’ve done some work in IFC, and have had it in the back of my mind to consider how it can be integrated with dependent types.

I agree that we need to express stronger properties, and some of that may be in the types, but there are other approaches as well. EG,

class BlockCipher bc => VerifiedBlockCipher bc where
  notIdentity : key -> block -> Not (block = encryptBlock key block)
  ...

This allows ciphers to be implemented more quickly, and then later have those security properties proven, while allowing users to constrain to only verified ciphers when possible (look at Prelude.Algebra for some examples of this). We could even use some psychological pressure to encourage the use of verified ciphers by doing

class BlockCipher k where
  weakEncryptBlock : k -> Bits bitsPerBlock -> Bits bitsPerBlock

class BlockCipher k => VerifiedBlockCipher where
  instance BlockCipher k where
    weakEncryptBlock = encryptBlock
  encryptBlock k -> BitsWithMoreProperties -> BitsWithMoreProperties

now every call with an unverified cipher nags at you. And properties that should hold only for particular ciphers can also be proven stand-alone (without affecting the type).

I’ve also been playing with some kind of wrapper type (I should make branches, to expose these experiments) to contain more arbitrary properties. Effectively, type Security = Insecure a | Unknown a | Secure a, where Secure a <*> Unknown b = Unknown (a <*> b), Unknown a <*> Insecure b = Insecure (a <*> b), and pure = Unknown. We can explicitly generate Insecure values whenever a known weak cipher is used, or a key is used to encrypt more blocks than is considered safe, etc. This is much more hand-wavy than proofs, but allows quick tagging as vulnerabilities are discovered, etc. The level could also be encoded in the type (as a Nat, perhaps) which would allow us to ensure, for example, that an unverified BlockCipher never returns a Secure value.

Expect wiki and branch updates today to reflect all of this rambling, and I am happy to accept any PRs that give us stronger guarantees.

[dckc]

OK, yes, I'm familiar with the unverified and verified Algebra stuff, and that's a reasonable approach.

And yes, please, use the psychological pressure. I suggest the shorter BlockCipher name for the type with more properties and a more obscure name a la UnverifiedDontUseThisUnlessYouReallyWantToPointTheGunAtYourOwnFootBlockCypher for the plain one. Perhaps weakEncryptBlock vs encryptBlock could get the message across, but even weakEncryptBlock suggests there's some sort of encryption going on. transformBlock comes to mind.

As to PRs, I'm afraid I'm a long way off from understanding how to port what I learned from rF* to idris. I had to look up IFC ;-)

[sellout]

I just pushed my current idea of the Security monad on its own branch: https://github.com/idris-hackers/idris-crypto/blob/Security-monad/src/Data/Crypto/Security.idr

Very open to suggestion.

[dckc]

I wonder if discrete labels like that are sufficiently expressive, or if things like "the attacker will have to explore on average 2^n guesses" will be needed.

Meanwhile... I found a link from the rF* style of types and proofs to Isabelle/HOL, and to my understanding, the Isabelle/HOL type system is in the same neighborhood as idris's.

This property we discharge using a relational proof
calculus [36], similar in style to the seminal work of
Benton [10] and other reasoning systems for confidentiality
properties [4], [5], with an automated verification condition
generator [14].

seL4: from General Purpose to a Proof of Information Flow Enforcement

The seL4 information flow security seems to use discrete labels too, so that approach does seem pretty useful.

[dckc]

updated link: https://www.microsoft.com/en-us/research/publication/probabilistic-relational-verification-for-cryptographic-implementations/