The Flow Caml system. The Flow Caml system is a prototype implementation of an information flow analyzer for the Caml language. It has been publicly announced on 2003-07-01. It consists in an extension of the OCaml 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. Flow Caml handles a large part of the OCaml language, including datatypes and pattern-matching, imperative features (mutable objects, exceptions, ...), and the module language. It can be used either as a standalone, batch-oriented compiler that produces regular OCaml code, or as an interactive, toplevel-based system.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Bartoletti, Massimo; Castellani, Ilaria; Deniélou, Pierre-Malo; Dezani-Ciancaglini, Mariangiola; Ghilezan, Silvia; Pantovic, Jovanka; Pérez, Jorge A.; Thiemann, Peter; Toninho, Bernardo; Vieira, Hugo Torres: Combining behavioural types with security analysis (2015)
- Schoepe, Daniel; Hedin, Daniel; Sabelfeld, Andrei: SeLINQ: tracking information across application-database boundaries (2014)
- Broberg, Niklas; van Delft, Bart; Sands, David: Paragon for practical programming with information-flow control (2013)
- Russo, Alejandro; Sabelfeld, Andrei: Securing interaction between threads and the scheduler in the presence of synchronization (2009)
- Hedin, Daniel; Sands, David: Timing aware information flow security for a javacard-like bytecode. (2005)