Lo scritto di ALF del 16.9.2015 si svolgerà alle ore 15.00 nel Laboratorio Magistrale del Palazzo delle Scienze.
Sep 152015
bart
Oct 242012
The PRIN 2010-11 project “Security Horizons” has been funded by the MIUR, with D. D. 23.10.2012 n. 719.
National coordinator: Pierpaolo Degano
Local coordinator: Massimo Bartoletti
Local coordinator: Massimo Bartoletti
Abstract.
Society increasingly depends on complex ecosystems of interacting software components. The number and variety of security-critical applications that rely on these systems has also grown over the years, and this trend will foreseably continue in the future. Despite of the applications being security-critical, they are still far from being secure: every day security researchers (and, more dangerously, hackers) discover new attacks to these systems. While perfect security is not a reachable goal, the current situation where security is intended as a marketing word and not as a concrete guarantee, can and must be improved.
Unfortunately, the problem of realizing software components that securely interact in an insecure environment is extremely hard to solve. This has many causes, among which the heterogeneity of the software components, the fact that they are controlled by different entities with possibly conflicting goals, the fact that attacks may take an unpredictable variety of different forms, etc.
A reasonable goal is to focus on some specific security properties, and prove that they are enjoyed by the application, even in the presence of attackers. This requires the development of new techniques to design, analyse, and implement software components. We are confident that Security Horizons will lead to an important advancement in that direction.
This project aims at developing a rigorous methodology and a language-based framework that will provide formal methods to support software engineers when they design, implement and maintain secure systems. This support will span all the software development phases: specification, design, implementation, validation, including verification and testing. To this end, we will study models and specification languages that allow one to formally express the many facets of online services and of their hosting infrastructures.
May 122012
Emilio Tuosto, Roberto Zunino and myself have developed a parametric calculus for contract-based computing in distributed systems. By abstracting from the actual contract language, our calculus generalises both the contracts-as-processes and contracts-as-formulae paradigms. The calculus features primitives for advertising contracts, for reaching agreements, and for querying the fulfilment of contracts. Coordination among participants happens via multi-party sessions, which are created once agreements are reached.
We present two instances of our calculus, by modelling contracts as processes in a variant of CCS, and as formulae in a logic. We formally relate the two paradigms, through an encoding from contracts-as-formulae to contracts-as-processes which ensures that the promises deducible in the logical system are exactly those reachable by its encoding as a process.
Finally, we present a coarse-grained taxonomy of possible misbehaviours in contract-oriented systems, and we illustrate them with the help of a variety of examples.
References
M. Bartoletti, E. Tuosto, R. Zunino. Contract-oriented Computing in CO2. In Scientific Annals of Computer Science, 22(1), 2012.
Mar 292012
Emilio Tuosto, Roberto Zunino and myself have developed a theory of contracting systems, where behavioural contracts may be violated by dishonest participants after they have been agreed upon – unlike in traditional approaches based on behavioural types.
We have considered the contracts of Castagna-Gesbert-Padovani, and we have embedded them in a calculus that allows distributed participants to advertise contracts, reach agreements, query the fulfilment of contracts, and realise them (or choose not to).
Our contract theory makes explicit who is culpable at each step of a computation. A participant is honest in a given context S when she is not culpable in each possible interaction with S. Our main result is a sufficient criterion for classifying a participant as honest in all possible contexts.
References
Massimo Bartoletti, Emilio Tuosto and Roberto Zunino. On the realizability of contracts in dishonest systems. To appear in Proc. COORDINATION, 2012
Sep 232011
My RAS Project TRICS: A Trusted Reservation Infrastructure for Computational Societies has been funded (grant L.R.7/2007 CRP-17285).
The goal of this project is to model and develop a trustworthy reservation infrastructure. We are looking for a generic infrastructure, which can be specialized to a wide variety of contexts of reservations: flights, hotels, museums, car pooling, medical examinations, etc.
A key aspect of the project is that the interaction between clients and services should be guided by contracts, which allow clients and services to agree on the required and offered features. Contracts might have, for example, sanctions for the modification or the cancellation of reservations, within agreed time limits. Contracts would be formal entities that would allow, on one side, to establish exactly and without uncertainty the obligations and rights of providers and clients and, on the other side, to formally verify whether or not services respect the advertised contracts. Furthermore, contracts will allow the client to compare different providers of the same service and to choose the most suitable for their desires.
The formal specification of contracts is a main research challenge, since one needs a comprehensive theoretical framework, capable of dealing with all the aspects (deadlines, reputation, sanctions, etc.) needed for modelling all the scenarios of interest.
A further goal of this project is the integration of the reservation infrastructure with social networks. In particular, we aim at developing search and recommendation algorithms to single out the services more suitable to the user needs. Such algorithms will be based both on single user profiling, and on the study of the relation with other users in the community.
Jul 012011
Emilio Tuosto, Roberto Zunino and myself have introduced a parametric calculus for contract-based computing in distributed systems. By abstracting from the actual contract language, our calculus generalises both the contracts-as-processes and contracts-as-formulae paradigms.
The calculus features primitives for advertising contracts, for reaching agreements, and for querying the fulfilment of contracts. Coordination among principals happens via multi-party sessions, which are created once agreements are reached.
We have presented two instances of our calculus, by modelling contracts as (i) processes in a variant of CCS, and (ii) as formulae in a logic. With the help of a few examples, we have discussed the primitives of our calculus, as well as some possible variants.
References
Massimo Bartoletti, Emilio Tuosto and Roberto Zunino. Contracts in Distributed Systems. In Proc. Interaction and Concurrency Experience (ICE), 2011
Dec 032010
by Tiziana Cimoli,
PhD student in Computer Science
Dipartimento di Matematica e Informatica,
Università degli Studi di Cagliari
The current version of kSOAP2, the Android library for communication via SOAP, does not offer facilities for serializing and deserializing complex objects. Furthermore, arrays are not supported.
In this post, we will introduce a patch of kSOAP2 which enables Android clients to communicate complex objects and arrays via SOAP. We will do that with the help of an example.
Here you can find:
Apr 022010
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).
Oct 122009
Roberto Zunino and myself have recently investigated the logical foundations of contracts in concurrent systems. A contract is an agreement stipulated between two or more parties, which specifies the duties and the rights of the parties involved therein. We have modelled contracts as formulae in an intuitionistic logic extended with a “contractual” form of implication. We have proved decidability of our logic via cut elimination: this allows us to mechanically infer the rights and the duties deriving from any set of contracts. We have embedded our logic in a core calculus of contracting processes, which combines features from concurrent constraints and calculi for multiparty sessions, while subsuming several idioms for concurrency. We have then shown how to exploit our calculus as a tool for modelling services, the interaction of which is driven by contracts.
References
- Massimo Bartoletti and Roberto Zunino. A calculus of contracting processes.
To appear in LICS 2010. A draft is available here. - Massimo Bartoletti and Roberto Zunino. A calculus of contracting processes.
Technical Report DISI-09-056, 2009. [pdf] - Massimo Bartoletti and Roberto Zunino. A logic for contracts.
Technical Report DISI-09-034, 2009. [pdf]
Nov 032008
Since Nov 3, 2008 I am a researcher at the Dipartimento di Matematica e Informatica, Università degli Studi di Cagliari.
I moved from the University of Pisa, where I got my PhD in 2005 at the Computer Science Department, with a thesis on static analysis for language-based security. From 2005 to 2008, I had two postdocs on programming languages security. Here you can find a full list of my publications, sorted by category.
