DepSec: Static Information-Flow Control in Idris

This repository contains DepSec, a dependently typed library for static information-flow control in Idris.

This repository is the accompanying code for the POST 2019 paper A Dependently Typed Library for Static Information-Flow Control in Idris by Simon Gregersen, Søren Eller Thomsen, and Aslan Askarov.

Prerequisites

DepSec has been built and tested using

• Idris 1.3.1.

Installation

Copy this package and run

$ idris --install depsec.ipkg

To use it in your program, run Idris with

$ idris -p depsec yourprogram.idr

Directory Structure

• DepSec - core library, together with declassification primitives
• Examples - case studies and examples from the paper