TESLA

My RAS Project TESLA: Techniques for Enforcing Security in Languages and Applications has been funded (grant L.R.7/2007-CRP2_120).

This project aims at fostering the understanding and the circulation of formal methods for security outside the academic context. We propose a vertical approach, where software security is considered at different levels of abstraction…

We start from a foundational level, where we consider idealised models of programming languages. At this level, we introduce various security models and policies, and we study techniques for their analysis and enforcement.

We then move to the programming languages level. At this more concrete level, we consider commercial programming languages, with Java as a primary target. Here, we are interested in studying refinements of the models and techniques developed at the foundational level. In particular, we want to assess how the augmented concreteness of the language affects the expressivity, decidability and complexity of the results obtained at the more abstract level.

Finally, we move to the application level, where we consider real-world scenarios to experiment with the techniques introduced above. In particular, we want to establish whether the models defined at the more abstract levels are expressive enough to deal with security policies occurring in realistic scenarios. Also, we aim at measuring the accuracy and efficiency of our analysis and enforcement techniques.

As a main case study and reality-check for the techniques developed in this project, we will model, analyse and develop a workflow management system for the dematerialization of the administrative documentation of the University of Cagliari.

This project has been funded by the Autonomous Region of Sardinia, with grant L.R.7/2007-CRP2_120. You can find the full version of the project proposal  here (in italian).