• Stars
    star
    120
  • Rank 295,907 (Top 6 %)
  • Language Idris
  • License
    BSD 3-Clause "New...
  • Created over 10 years ago
  • Updated over 6 years ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Implementation of cryptographic primitives using Idris

idris-crypto

Join the chat at https://gitter.im/idris-hackers/idris-crypto

This project looks to develop cryptographic primitives using the general purpose functional language Idris.

It is important to note that the Idris language is first and foremost a research project, and thus the tooling provided by idris-crypto should not necessarily be seen as production ready nor for industrial use.

Motivation

Cryptography is something that is important to get right. It is also difficult to get right. Most languages make it too easy to shoot yourself in the foot (buffer overflows, gotos, etc.) and even those that donโ€™t offer limited help, but some languages make it possible to prove arbitrary properties of a program and this ability can give you more confidence that your program is doing what it should. However, a cryptography library also needs to be readily usable by other software, hopefully not tied to code written in its implementation language.

Idris is a win on both sides here. On the one hand, it allows us to prove things about the code, but unlike other proof assistants has LLVM and JS backends, which means that it can be linked to very much like a C library, and can also be used by JS, on both the server and client side. It is in a relatively unique position that is ideal for crypto.

Note on Security

The security of cryptographic software libraries and implementations is a tricky thing to get right. The notion of what makes a cryptographic software library secure can be a highly contested subject. It is not good enough that a crypto software library is just functionally correct, and contains no coding errors. A secure cryptographic software library needs to be resitant to many types of attack for instance:

  • Software bugs
  • Lack of adherence to a specification
  • Use of a poor specification
  • Use of poor primitives
  • Side Channel Attacks
  • Using unproven math
  • Use of provably secure crypto
  • the list goes on and on and on.

A language that is safer than C only gets you so far. However, the use of a general purpose language that supports:

  • full dependent types,
  • totality checking,
  • tactic based theorem proving,
  • code generation to other languages

arguably provides an really interesting development environment in which to explore the development of possibly provably secure and demonstrably correct cryptographic primitives.

Which primitives

The list of supported primitives will be summarised here.

Encryption

  • DES insecure
  • Triple DES
  • ARC4 insecure

MAC / cryptographic hash

  • SHA-1 (and the rest of the SHS functions โ€“ SHA-256, SHA-512, etc.)

Usage

The easiest way to use the library is simply using encrypt/decrypt. You can pass it either a stream cipher, or a pair of a block cypher and encryption mode:

> the String (encrypt (ARC4 key) "some message")
"cuhrclh,.urch,.lih.ulchu" : String
> the String (decrypt (TDEA1 [key, key, key], CFB iv) "t893gy'c.,aihntebgl'"
"some message" : String

If you already have lists of bytes, try encryptMessage/decryptMessage instead.

The other useful pair of operations is specific to stream ciphers:

> decryptStream (ARC4 key) stream
? : Stream

and now youโ€™re pipelining!

Plans / Notes

  • Get a couple of the more common primitives for each type of function

  • work on getting something that is easily usable via an FFI

  • prove interesting properties about various primitives (look in papers for these)

  • start building up higher-level components / protocols

  • MOAR PRIMITIVES

  • would be nice to require that insecure primitives run inside of some monad, but need some restricted escape mechanism so, EG, TDEA can be secure while DEA isnโ€™t.

  • for DSA, implement it deterministically, both to avoid bad pRNGs (which we should do in general), but also just because determinism is nice

Contributions

Every contribution is appreciated โ€“ from documentation, to fixing typos, to adding one little function to a data structure. Even if youโ€™re just touching Idris, dependent types, etc. for the first time. Join in!

More Repositories

1

software-foundations

Software Foundations in Idris
Idris
453
star
2

idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
Emacs Lisp
256
star
3

idris-vim

Idris mode for vim
Vim Script
223
star
4

idris-demos

Collection of Idris tests and demonstration programs
Idris
189
star
5

idris-koans

Koans are small lessons on the path to enlightenment. The aim of the Idris Koans project is to provide an easy learning environment in Idris. Your insight will be derived by encountering failing code and fixing them so that they type check.
Idris
172
star
6

IdrisWeb

A secure web framework, built in the Idris language.
TeX
108
star
7

atom-language-idris

A Idris Mode for Atom.io
TypeScript
99
star
8

IdrisScript

FFI Bindings to interact with the unsafe world of JavaScript
Idris
88
star
9

idris-llvm

Idris LLVM codegen factored out
Haskell
77
star
10

idris-java

Java Code Generator for Idris
Haskell
71
star
11

iQuery

Idris Lib to interact with the DOM and Browser API for the JavaScript backend
Idris
40
star
12

idris-posix

System POSIX bindings for Idris.
Idris
34
star
13

idrispkgs

Old Nix expressions for Idris packaging. Idris support moved into Nixpkgs!
Nix
28
star
14

idris-sublime

A Plugin to use Idris with Sublime
Python
27
star
15

idris-free

Free Monads and useful constructions to work with them
Idris
25
star
16

eff-tutorial

An old tutorial for using `Effects` in Idris.
TeX
24
star
17

idris-cph-exercises

Exercises from the Idris lecture series presented at the ITU Copenhagen on March 11--15, updated to work with latest Idris releases.
Idris
23
star
18

idris-lens

Idris
22
star
19

idris-algebra

This is an attempt at painting as many bikesheds as possible with a typeclass hierarchy for idris reflecting "Algebra"
Idris
18
star
20

usb

libusb binding for idris and Effectful USB programming
C
11
star
21

idris-bot

An IRC bot connected to an Idris REPL
Haskell
10
star
22

idris-java-rts

Java Runtime System for the Idris Programming Language
Java
10
star
23

idris-extras

Various minor modes for editors and some tool support.
TeX
6
star
24

idris-array

primitive flat arrays containing Idris values
Idris
6
star
25

idris-time

A dependently-typed implementation of ISO 8601.
3
star