|Home \ Graduation Activities \ Post-Graduation Page||Login|
Information Flow Analysis using Data-dependent Logical Propositions
A significant number of today’s software systems are designed around database sys- tems that store business information, as well as data relevant to access control enforce- ment, such as user profiles and permissions. Thus, the code implementing security mech- anisms is scattered across the application code, often replicated at different architectural layers, each one written in its own programming language and with its own data format. Several approaches address this problem by integrating the development of all applica- tion layers in a single programming language. For instance, languages like Ur/Web and LiveWeb/λDB provide static verification of security policies related to access control, en- suring that access control code is correctly placed. However, these approaches provide limited support to the task of ensuring that information is not indirectly leaked because of implementation errors. In this thesis, we present a type-based information-flow analysis for a core language based in λDB, whose 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. In order to validate our approach, we discuss the imple- mentation of a proof-of-concept extension to the LiveWeb framework and the concerns involved in the development of a medium-sized application in our language.
Post-Graduation Student / Researcher / Professor: