TESLA

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

Publications

2013

  • 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

2012

  • R. Bardou, R. Focardi, Y. Kawamoto, L. Simionato, G. Steel, J. Tsay. Efficient Padding Oracle Attacks on Cryptographic Hardware. In CRYPTO 2012
  • M. Bartoletti, T. Cimoli, G.M. Pinna and R. Zunino. Circular causality in event structures. In ICTCS, 2012.
  • M. Bartoletti, E. Tuosto, R. Zunino. On the realizability of contracts in dishonest systems. In Proc. COORDINATION, 2012. Also available as CoRR abs/1201.6188, 2012.
  • M. Bartoletti, E. Tuosto, R. Zunino. Contract-oriented Computing in CO2. In Scientific Annals of Computer Science, 22(1), 2012.
  • M. Bartoletti, T. Cimoli, G.M. Pinna and R. Zunino. An event-based model for contracts. In Proc. PLACES, 2012.
  • C. Bodei, P. Degano, G.L. Ferrari, L. Galletta and G. Mezzetti. Formalising Security in Ubiquitous and Cloud Scenarios. In Proc. 11th IFIP TC 8 International Conference on Computer Information Systems and Industrial Management, 2012
  • M. Bugliesi, S. Calzavara, R. Focardi, M. Squarcina. Gran: Model Checking Grsecurity RBAC Policies. In IEEE CSF 2012
  • M. Centenaro, R. Focardi, F. L. Luccio. Type-Based Analysis of PKCS#11 Key Management. In POST, 2012
  • G. Costa, P. Degano and F. Martinelli. Modular plans for secure service composition. Journal of Computer Security 20(1), 2012
  • G. Costantini, P. Ferrara and A. Cortesi. Linear approximation of continuous systems with Trapezoid Step Functions in Jhala. In APLAS 2012
  • G. Ciobanu and G.M. Pinna. Catalytic Petri Nets are Turing Complete. In Proc. LATA, 2012.
  • P. Degano, G.L. Ferrari and G. Mezzetti. Nominal Automata for Resource Usage Control. In Proc. CIIA, 2012
  • P. Degano, G.L. Ferrari, L. Galletta and G. Mezzetti. Typing Context-Dependent Behavioural Variations. In Proc. PLACES, 2012.
  • P. Degano, G.L. Ferrari, L. Galletta and G. Mezzetti. Types for Coordinating Secure Behavioural Variations. In Proc. COORDINATION, 2012
  • R. Halder and A. Cortesi. Abstract Interpretation of Database Query Languages. In Computer Languages, Systems & Structures 38(2), 2012
  • M. Zanioli, P. Ferrara and A. Cortesi. SAILS: Static Analysis of Information Leakage with Sample. In Proc. 27th ACM Symposium on Applied Computing, 2012
  • R. Halder and A. Cortesi. Tukra: An Abstract Program Slicing Tool. In Proc. ICSOFT, 2012

2011

  • M.S. Alvim, M.E. Andrés, K. Chatzikokolakis, P. Degano and C. Palamidessi. Differential Privacy: on the trade-off between Utility and Information Leakage. In Proc. Formal Aspects of Security and Trust (FAST), 2011
  • M. Bartoletti, E. Tuosto and R. Zunino. Contracts in Distributed Systems. In Proc. Interaction and Concurrency Experience (ICE), 2011
  • S. Bhattacharya and A. Cortesi. Property Driven Program Slicing Refinement. In Proc. 6th International Conference on Software and Database Technologies (ICSOFT), 2011
  • C. Bodei, V.D. Dinh and G.L. Ferrari. Predicting global usages of resources endowed with local policies. In Proc. FOCLASA, 2011
  • A. Cortesi and M. Zanioli. Widening and Narrowing Operators for Abstract Interpretation. Computer Languages, Systems and Structures. Volume 37(1), pp. 24-42, Elsevier, 2011
  • G. Costantini, P. Ferrara, A. Cortesi. Static Analysis of String Values. In Proc. 13th International Conference on Formal Engineering Methods (ICFEM), 2011
  • P. Degano, G.L. Ferrari and G. Mezzetti. On quantitative security policies. In Proc. PACT, 2011
  • R. Focardi, F. Luccio and G. Steel. An Introduction to Security API Analysis. In Proc. Foundations of Security Analysis and Design (FOSAD), 2011.
  • R. Focardi and F. Luccio. Secure recharge of disposable RFID tickets. In Proc. Formal Aspects of Security and Trust (FAST), 2011
  • R. Halder and A. Cortesi. Cooperative Query Answering by Abstract Interpretation. In Proc. 37th International Conference on Current Trends in Theory and Practice of Computer Science. Lecture Notes in Computer Science, vol. 6543, pp. 284-296, Springer, 2011
  • R. Halder and A. Cortesi. Observation-based Fine Grained Access Control for XML Documents. In Proc. 10th International Conference on Computer Information Systems and Industrial Management Applications (CISIM), 2011. Communications in Computer and Information Science (to appear)
  • G.M. Pinna. How much is worth to remember ? A taxonomy based on Petri Nets unfoldings. In Proc. Petri Nets, 2011
  • M. Zanioli and A. Cortesi. Information Leakage Analysis by Abstract Interpretation. In Proc. 37th International Conference on Current Trends in Theory and Practice of Computer Science. Lecture Notes in Computer Science, vol. 6543, pp. 545-557 Springer, 2011

2010