Information flow analysis using data-dependent logical propositions

Dissertação para obtenção do Grau de Mestre em Engenharia Informática

A significant number of today’s software systems are designed around database systems that store business information, as well as data relevant to access control enforcement, such as user profiles and permissions. Thus, the code implementing security mechanisms 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 application layers in a single programming language. For instance, languages like Ur/Web and LiveWeb/lDB provide static verification of security policies related to access control, ensuring 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 lDB, whose security levels are logical propositions depending on actual data. This approach allows for an accurate tracking of information throughout a databasebacked 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 implementation 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.