Security Horizons

Unica Commenti disabilitati

Ott 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 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 [...]

Contract-oriented Computing in CO2

Unica Commenti disabilitati

Mag 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 [...]

On the realizability of contracts in dishonest systems

Unica Commenti disabilitati

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 [...]

TRICS

Unica Commenti disabilitati

Set 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 [...]

Contracts in Distributed Systems

Unica Commenti disabilitati

Lug 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 [...]

kSOAP2 patch for user-defined objects and arrays

Unica Commenti disabilitati

Dic 032010

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: * the jar of our patch * the sources of the patched files * the sources of the example (both client and server) * the sources of the official version of kSOAP2.

TESLA

Unica Commenti disabilitati

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 [...]

A Calculus of Contracting Processes

Unica Commenti disabilitati

Ott 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 [...]

contatti | accessibilità

Università degli Studi di Cagliari
C.F.: 80019600925 - P.I.: 00443370929

note legali | privacy