Skip to content
Timing attack resistant type systems
Idris
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
src/Timing
.gitignore
README.md
tarts.ipkg

README.md

TARTS

This is a project that aims to build systems that are provably immune to timing attacks. This is accomplished by using dependant types and the Curry-Howard isomorphism to have the program itself serve as the proof of its time constancy. At the moment the only function written is equality, and the proof is just that the same number of basic Boolean logical operations is performed, but the concept can be expanded to any function that can be expressed as a sequence of primitive boolean logical operations.

Note:

Everything is fairly broken right now as this is still really early pre-alpha

Accepted for presentation at THOTCON 2015!

You can’t perform that action at this time.