This prototype is the implementation of the work entitled "Information Flow Analysis using Data-dependent Logical Propositions", that extends the language of [1] with an information flow mechanism based on a lattice of logical expressions.
In this prototype, we present the extension of the LiveWeb framework with a type-based information-flow analysis, initially designed for a core language based in λDB. In this language the security levels are logical propositions depending on actual data. This approach allows for an accurate tracking of information throughout a database-backed software system, statically detecting the information leaks that may occur, with precision at the table-cell level.
[1] Caires, L., Jorge A. Perez, J. C. Seco, Hugo T. Vieira, and Lúcio Ferrão. "Type-based Access Control in Data-Centric Systems." Programming Languages and Systems, 20th European Symposium on Programming, ESOP 2011. Ed. Gilles Barthe. Lecture Notes in Computer Science. Springer-Verlag, 2011.