F* extends core-ML with a type system based on dependent refinements, higher kinds and affine types. It enables verification of higher-order stateful programs with automation via SMT solving.
Date: 2 September 2013
Size: 35.50 MB
Automata is a .NET tool kit that provides facilities for manipulating and analyzing regular expressions, symbolic finite automata, and symbolic finite transducers. It supports automata and transducers where input and output alphabets can be fully symbolic. Constraints over the alphabets can be analyzed using Satisfiability Modulo Theory (SMT) solvers. The tool kit provides a particular extension that uses the Microsoft SMT solver Z3.
Date: 27 October 2011
Size: 3.13 MB
Memoir is a framework for building trusted modules with state continuity. The framework is described in our paper, Memoir: Practical State Continuity for Protected Modules.
Date: 5 April 2011
Size: 0.18 MB
Research and analysis related to computer networks is often hampered by the tension between the need for accurate network packet traces to study, and the concern that these traces may contain sensitive information. Starting from recent work on differential privacy, we have produced a toolkit and a collection of standard network trace analyses using these tools that guarantee differential privacy. The download demonstrates the tools, and how they can be used to analyze network trace data while providing...
Date: 18 August 2010
Size: 0.16 MB
This is a source release of the Fine compiler and several example programs. The Fine compiler implements a type system that enables the enforcement of rich, stateful authorization and information-flow policies to be verified. Our compilation technique produces verifiable target code in a language called DCIL, an extension of CIL, the language of the .NET runtime. Code consumers can check DCIL target programs using a syntactic byte-code verifier to establish the security of the code.
Date: 28 May 2010
Size: 4.92 MB
Privacy Integrated Queries (PINQ) is a LINQ-like API for writing programs against sensitive data sets, while providing differential privacy guarantees for the underlying records. This first release provides the PINQ infrastructure, several example data analysis applications, and should be suitable for prototyping many differentially-private data analyses.
Date: 18 August 2009
Size: 0.27 MB
FS2PV is a verification tool that compiles cryptographic-protocol implementations in a first-order subset of F# to a formal pi-calculus model. This pi-calculus model then can be analyzed using ProVerif to prove the desired security properties or to find security flaws.
Date: 14 February 2007
Size: 2.19 MB
TulaFale is a new specification language for writing machine-checkable descriptions of SOAP-based security protocols and their properties. TulaFale is based on the pi calculus (for writing collections of SOAP processors running in parallel), plus XML syntax (to express SOAP messaging), logical predicates (to construct and filter SOAP messages), and correspondence assertions (to specify authentication goals of protocols). Our implementation compiles TulaFale into the applied pi calculus, and then runs...
Date: 15 May 2006
Size: 2.24 MB