arXiv subjects

Letterio Galletta

Publications and source records attributed to Letterio Galletta.

24 records · Page 2Linked to original sources

arXiv2017

Tracing where IoT data are collected and aggregated

The Internet of Things (IoT) offers the infrastructure of the information society. It hosts smart objects that automatically collect and exchange data of various kinds, directly gathered from sensors or generated by aggregations. Suitable coordination primitives and analysis mechanisms are in order to design and reason about IoT systems, and to intercept the implied technological shifts. We address these issues from a foundational point of view. To study them, we define IoT-LySa, a process calculus endowed with a static analysis that tracks the provenance and the manipulation of IoT data, and how they flow in the system. The results of the analysis can be used by a designer to check the behaviour of smart objects, in particular to verify non-functional properties, among which security.

cs.PL↗

arXiv2016

A Step Towards Checking Security in IoT

The Internet of Things (IoT) is smartifying our everyday life. Our starting point is IoT-LySa, a calculus for describing IoT systems, and its static analysis, which will be presented at Coordination 2016. We extend the mentioned proposal in order to begin an investigation about security issues, in particular for the static verification of secrecy and some other security properties.

cs.PL↗

arXiv2016

Event-driven Adaptation in COP

Context-Oriented Programming languages provide us with primitive constructs to adapt program behaviour depending on the evolution of their operational environment, namely the context. In previous work we proposed ML_CoDa, a context-oriented language with two-components: a declarative constituent for programming the context and a functional one for computing. This paper describes an extension of ML_CoDa to deal with adaptation to unpredictable context changes notified by asynchronous events.

cs.PL↗

arXiv2015

A Context-Oriented Extension of F#

Context-Oriented programming languages provide us with primitive constructs to adapt program behaviour depending on the evolution of their operational environment, namely the context. In previous work we proposed ML_CoDa, a context-oriented language with two-components: a declarative constituent for programming the context and a functional one for computing. This paper describes the implementation of ML_CoDa as an extension of F#.

cs.PL↗

arXiv2013

Typing Context-Dependent Behavioural Variation

Context Oriented Programming (COP) concerns the ability of programs to adapt to changes in their running environment. A number of programming languages endowed with COP constructs and features have been developed. However, some foundational issues remain unclear. This paper proposes adopting static analysis techniques to reason on and predict how programs adapt their behaviour. We introduce a core functional language, ContextML, equipped with COP primitives for manipulating contexts and for programming behavioural variations. In particular, we specify the dispatching mechanism, used to select the program fragments to be executed in the current active context. Besides the dynamic semantics we present an annotated type system. It guarantees that the well-typed programs adapt to any context, i.e. the dispatching mechanism always succeeds at run-time.

cs.PL↗

arXiv2011

An Abstract Semantics for Inference of Types and Effects in a Multi-Tier Web Language

Types-and-effects are type systems, which allow one to express general semantic properties and to statically reason about program's execution. They have been widely exploited to specify static analyses, for example to track computational side effects, exceptions and communications in concurrent programs. In this paper we adopt abstract interpretation techniques to reconstruct (following the Cousot's methodology) a types-and-effects system developed to handle security problems of a multi-tier web language. Our reconstruction allows us to show that this types-and-effects system is not sound with respect to the semantics of the language. In addition, we correct the soundness issues in the analysis and systematically construct a correct analyser.

cs.LO↗