|
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
|
|
Flow Caml
