Projects‎ > ‎


Techniques for Enforcing Security in Languages and Applications

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.

Project Members

Università degli Studi di Cagliari - Dipartimento di Matematica e Informatica
  • Massimo Bartoletti (project coordinator)
  • G. Michele Pinna
  • Riccardo Scateni
  • Paolo di Giamberardino
  • Tiziana Cimoli
Università di Pisa - Dipartimento di Informatica
  • Pierpaolo Degano
  • Gian Luigi Ferrari
  • Chiara Bodei
  • Emilio Tuosto (University of Leicester)
Università Ca' Foscari Venezia - Dipartimento di Informatica
  • Agostino Cortesi
  • Riccardo Focardi
  • Flaminia Luccio
  • Sukriti Bhattacharya
  • Alberto Carraro
  • Matteo Centenaro
  • Pietro Ferrara
  • Raju Halder
  • Matteo Zanioli



  • M. Bartoletti, P. Degano, G. Ferrari and R. Zunino. Model checking usage policies. To appear in Mathematical Structures in Computer Science.
  • M. Bartoletti, T. Cimoli and R. Zunino. A theory of agreements and protection. In Proc. POST 2013.
  • M. Bartoletti, T. Cimoli and G.M. Pinna. Lending Petri nets and contracts. To be presented at FSEN 2013. Also available as CoRR abs/1211.3624.
  • M. Bartoletti, A. Scalas, E. Tuosto, R. Zunino. Honesty by typing. Presented at BEAT 2013. Also available as CoRR abs/1211.2609.
  • S. Bhattacharya and A. Cortesi. Distortion-Free Authentication Watermarking. Software and Data Technologies, in Communications in Computer and Information Science. Springer Verlag, vol. 170, 2013
  • R. Halder and A. Cortesi. Abstract program slicing on dependence condition graphs. In Science of Computer Programming ((ISSN 0167-6423). To appear.
  • R. Halder and A. Cortesi. Fine Grained Access Control for Relational Databases by Abstract Interpretation. Software and Data Technologies, in Communications in Computer and Information Science. Springer Verlag, 170, 2013




Massimo Bartoletti,
Nov 4, 2011, 4:59 AM
Massimo Bartoletti,
Sep 14, 2011, 2:18 PM
Massimo Bartoletti,
Sep 14, 2011, 2:19 PM
Massimo Bartoletti,
Sep 14, 2011, 2:18 PM