Lambda the Ultimate

inactiveTopic Flow Caml
started 7/2/2003; 4:46:22 AM - last post 7/2/2003; 4:46:22 AM
Ehud Lamm - Flow Caml  blueArrow
7/2/2003; 4:46:22 AM (reads: 1166, responses: 0)
Flow Caml
Flow Caml is an extension of the Objective Caml language with a type system tracing information flow. Its purpose is basically to allow to write "real" programs and to automatically check that they obey some confidentiality or integrity policy. In Flow Caml, standard ML types are annotated with security levels chosen in a user-definable lattice. Each annotation gives an approximation of the information that the described expression may convey. Because it has full type inference, the system verifies, without requiring source code annotations, that every information flow caused by the analyzed program is legal with regard to the security policy specified by the programmer.

Technically speaking, Flow Caml is also one of the first real-size implementations of a programming language equipped with a type system that features simultaneously subtyping, ML polymorphism and full type inference.

Here's a very clear explanation of the basic concept.

Section 2.1 of the manual contains several simple examples that will be helpful for understanding how such a system can be used.

Posted to Software-Eng by Ehud Lamm on 7/2/03; 4:52:36 AM