Comments (5)
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.
from idris-crypto.
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 ;-)
from idris-crypto.
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.
from idris-crypto.
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.
from idris-crypto.
updated link: https://www.microsoft.com/en-us/research/publication/probabilistic-relational-verification-for-cryptographic-implementations/
from idris-crypto.
Related Issues (4)
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from idris-crypto.