Showing 1–21 of 21 results for author: Galletta, L

Policies for Fair Exchanges of Resources

Authors: Lorenzo Ceragioli, Pierpaolo Degano, Letterio Galletta, Luca Viganò

Abstract: People increasingly use digital platforms to exchange resources in accordance to some policies stating what resources users offer and what they require in return. In this paper, we propose a formal model of these environments, focussing on how users' policies are defined and enforced, so ensuring that malicious users cannot take advantage of honest ones. To that end, we introduce the declarative p… ▽ More People increasingly use digital platforms to exchange resources in accordance to some policies stating what resources users offer and what they require in return. In this paper, we propose a formal model of these environments, focussing on how users' policies are defined and enforced, so ensuring that malicious users cannot take advantage of honest ones. To that end, we introduce the declarative policy language MuAC and equip it with a formal semantics. To determine if a resource exchange is fair, i.e., if it respects the MuAC policies in force, we introduce the non-standard logic MuACL that combines non-linear, linear and contractual aspects, and prove it decidable. Notably, the operator for contractual implication of MuACL is not expressible in linear logic. We define a semantics preserving compilation of MuAC policies into MuACL, thus establishing that exchange fairness is reduced to finding a proof in MuACL. Finally, we show how this approach can be put to work on a blockchain to exchange non-fungible tokens. △ Less

Submitted 28 October, 2024; originally announced October 2024.

A Logic for Policy Based Resource Exchanges in Multiagent Systems

Authors: Lorenzo Ceragioli, Pierpaolo Degano, Letterio Galletta, Luca Viganò

Abstract: In multiagent systems autonomous agents interact with each other to achieve individual and collective goals. Typical interactions concern negotiation and agreement on resource exchanges. Modeling and formalizing these agreements pose significant challenges, particularly in capturing the dynamic behaviour of agents, while ensuring that resources are correctly handled. Here, we propose exchange envi… ▽ More In multiagent systems autonomous agents interact with each other to achieve individual and collective goals. Typical interactions concern negotiation and agreement on resource exchanges. Modeling and formalizing these agreements pose significant challenges, particularly in capturing the dynamic behaviour of agents, while ensuring that resources are correctly handled. Here, we propose exchange environments as a formal setting where agents specify and obey exchange policies, which are declarative statements about what resources they offer and what they require in return. Furthermore, we introduce a decidable extension of the computational fragment of linear logic as a fundamental tool for representing exchange environments and studying their dynamics in terms of provability. △ Less

Submitted 18 August, 2024; originally announced August 2024.

Explainable Ponzi Schemes Detection on Ethereum

Authors: Letterio Galletta, Fabio Pinelli

Abstract: Blockchain technology has been successfully exploited for deploying new economic applications. However, it has started arousing the interest of malicious actors who deliver scams to deceive honest users and to gain economic advantages. Ponzi schemes are one of the most common scams. Here, we present a classifier for detecting smart Ponzi contracts on Ethereum, which can be used as the backbone for… ▽ More Blockchain technology has been successfully exploited for deploying new economic applications. However, it has started arousing the interest of malicious actors who deliver scams to deceive honest users and to gain economic advantages. Ponzi schemes are one of the most common scams. Here, we present a classifier for detecting smart Ponzi contracts on Ethereum, which can be used as the backbone for developing detection tools. First, we release a labelled data set with 4422 unique real-world smart contracts to address the problem of the unavailability of labelled data. Then, we show that our classifier outperforms the ones proposed in the literature when considering the AUC as a metric. Finally, we identify a small and effective set of features that ensures a good classification quality and investigate their impacts on the classification using eXplainable AI techniques. △ Less

Submitted 18 April, 2024; v1 submitted 12 January, 2023; originally announced January 2023.

Comments: Accepted to ACM SAC'24

Automatic Fair Exchanges

Authors: Lorenzo Ceragioli, Letterio Galletta, Pierpaolo Degano, Luca Viganò

Abstract: In a decentralized environment, exchanging resources requires users to bargain until an agreement is found. Moreover, human agreements involve a combination of collaborative and selfish behavior and often induce circularity, complicating the evaluation of exchange requests. We introduce MuAC, a policy language that allows users to state in isolation under which conditions they are open to grant th… ▽ More In a decentralized environment, exchanging resources requires users to bargain until an agreement is found. Moreover, human agreements involve a combination of collaborative and selfish behavior and often induce circularity, complicating the evaluation of exchange requests. We introduce MuAC, a policy language that allows users to state in isolation under which conditions they are open to grant their resources and what they require in return. In MuAC, exchange requests are evaluated automatically with the guarantee that the only exchanges that will take place are those that mutually satisfy users' conditions. Moreover, MuAC can be used as an enforcement mechanism to prevent users from cheating. As a proof of concept, we implement a blockchain smart contract that allows users to exchange their non-fungible tokens. △ Less

Submitted 25 July, 2022; originally announced July 2022.

IFCIL: An Information Flow Configuration Language for SELinux (Extended Version)

Authors: Lorenzo Ceragioli, Letterio Galletta, Pierpaolo Degano, David Basin

Abstract: Security Enhanced Linux (SELinux) is a security architecture for Linux implementing mandatory access control. It has been used in numerous security-critical contexts ranging from servers to mobile devices. But this is challenging as SELinux security policies are difficult to write, understand, and maintain. Recently, the intermediate language CIL was introduced to foster the development of high-le… ▽ More Security Enhanced Linux (SELinux) is a security architecture for Linux implementing mandatory access control. It has been used in numerous security-critical contexts ranging from servers to mobile devices. But this is challenging as SELinux security policies are difficult to write, understand, and maintain. Recently, the intermediate language CIL was introduced to foster the development of high-level policy languages and to write structured configurations. However, CIL lacks mechanisms for ensuring that the resulting configurations obey desired information flow policies. To remedy this, we propose IFCIL, a backward compatible extension of CIL for specifying fine-grained information flow requirements for CIL configurations. Using IFCIL, administrators can express, e.g., confidentiality, integrity, and non-interference properties. We also provide a tool to statically verify these requirements. △ Less

Submitted 31 May, 2022; originally announced May 2022.

Comments: Extended version of the paper "IFCIL: An Information Flow Configuration Language for SELinux"

A theory of transaction parallelism in blockchains

Authors: Massimo Bartoletti, Letterio Galletta, Maurizio Murgia

Abstract: Decentralized blockchain platforms have enabled the secure exchange of crypto-assets without the intermediation of trusted authorities. To this purpose, these platforms rely on a peer-to-peer network of byzantine nodes, which collaboratively maintain an append-only ledger of transactions, called blockchain. Transactions represent the actions required by users, e.g. the transfer of some units of cr… ▽ More Decentralized blockchain platforms have enabled the secure exchange of crypto-assets without the intermediation of trusted authorities. To this purpose, these platforms rely on a peer-to-peer network of byzantine nodes, which collaboratively maintain an append-only ledger of transactions, called blockchain. Transactions represent the actions required by users, e.g. the transfer of some units of crypto-currency to another user, or the execution of a smart contract which distributes crypto-assets according to its internal logic. Part of the nodes of the peer-to-peer network compete to append transactions to the blockchain. To do so, they group the transactions sent by users into blocks, and update their view of the blockchain state by executing these transactions in the chosen order. Once a block of transactions is appended to the blockchain, the other nodes validate it, re-executing the transactions in the same order. The serial execution of transactions does not take advantage of the multi-core architecture of modern processors, so contributing to limit the throughput. In this paper we develop a theory of transaction parallelism for blockchains, which is based on static analysis of transactions and smart contracts. We illustrate how blockchain nodes can use our theory to parallelize the execution of transactions. Initial experiments on Ethereum show that our technique can improve the performance of nodes. △ Less

Submitted 17 November, 2021; v1 submitted 27 November, 2020; originally announced November 2020.

Comments: arXiv admin note: text overlap with arXiv:1905.04366

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 4 (November 18, 2021) lmcs:6935

Private-Yet-Verifiable Contact Tracing

Authors: Andrea Canidio, Gabriele Costa, Letterio Galletta

Abstract: We propose PrYVeCT, a private-yet-verifiable contact tracing system. PrYVeCT works also as an authorization framework allowing for the definition of fine-grained policies, which a certain facility can define and apply to better model its own access rules. Users are authorized to access the facility only when they exhibit a contact trace that complies with the policy. The policy evaluation process… ▽ More We propose PrYVeCT, a private-yet-verifiable contact tracing system. PrYVeCT works also as an authorization framework allowing for the definition of fine-grained policies, which a certain facility can define and apply to better model its own access rules. Users are authorized to access the facility only when they exhibit a contact trace that complies with the policy. The policy evaluation process is carried out without disclosing the personal data of the user. At the same time, each user can prove to a third party (e.g., a public authority) that she received a certain authorization. PrYVeCT takes advantage of oblivious automata evaluation to implement a privacy-preserving policy enforcement mechanism. △ Less

Submitted 19 October, 2020; originally announced October 2020.

Comments: Submitted for publication

A type language for message passing component-based systems

Authors: Zorica Savanović, Letterio Galletta, Hugo Torres Vieira

Abstract: Component-based development is challenging in a distributed setting, for starters considering programming a task may involve the assembly of loosely-coupled remote components. In order for the task to be fulfilled, the supporting interaction among components should follow a well-defined protocol. In this paper we address a model for message passing component-based systems where components are asse… ▽ More Component-based development is challenging in a distributed setting, for starters considering programming a task may involve the assembly of loosely-coupled remote components. In order for the task to be fulfilled, the supporting interaction among components should follow a well-defined protocol. In this paper we address a model for message passing component-based systems where components are assembled together with the protocol itself. Components can therefore be independent from the protocol, and reactive to messages in a flexible way. Our contribution is at the level of the type language that allows to capture component behaviour so as to check its compatibility with a protocol. We show the correspondence of component and type behaviours, which entails a progress property for components. △ Less

Submitted 16 September, 2020; originally announced September 2020.

Comments: In Proceedings ICE 2020, arXiv:2009.07628

ACM Class: F.3.1; F.3.2

Journal ref: EPTCS 324, 2020, pp. 3-24

Control-flow Flattening Preserves the Constant-Time Policy (Extended Version)

Authors: Matteo Busi, Pierpaolo Degano, Letterio Galletta

Abstract: Obfuscating compilers protect a software by obscuring its meaning and impeding the reconstruction of its original source code. The typical concern when defining such compilers is their robustness against reverse engineering and the performance of the produced code. Little work has been done in studying whether the security properties of a program are preserved under obfuscation. In this paper we s… ▽ More Obfuscating compilers protect a software by obscuring its meaning and impeding the reconstruction of its original source code. The typical concern when defining such compilers is their robustness against reverse engineering and the performance of the produced code. Little work has been done in studying whether the security properties of a program are preserved under obfuscation. In this paper we start addressing this problem: we consider control-flow flattening, a popular obfuscation technique used in industrial compilers, and a specific security policy, namely constant-time. We prove that this obfuscation preserves the policy, i.e., that every program satisfying the policy still does after the transformation. △ Less

Submitted 12 March, 2020; originally announced March 2020.

Comments: Extended version of ITASEC20 camera ready paper

Provably Secure Isolation for Interruptible Enclaved Execution on Small Microprocessors: Extended Version

Authors: Matteo Busi, Job Noorman, Jo Van Bulck, Letterio Galletta, Pierpaolo Degano, Jan Tobias Mühlberg, Frank Piessens

Abstract: Computer systems often provide hardware support for isolation mechanisms like privilege levels, virtual memory, or enclaved execution. Over the past years, several successful software-based side-channel attacks have been developed that break, or at least significantly weaken the isolation that these mechanisms offer. Extending a processor with new architectural or micro-architectural features, bri… ▽ More Computer systems often provide hardware support for isolation mechanisms like privilege levels, virtual memory, or enclaved execution. Over the past years, several successful software-based side-channel attacks have been developed that break, or at least significantly weaken the isolation that these mechanisms offer. Extending a processor with new architectural or micro-architectural features, brings a risk of introducing new such side-channel attacks. This paper studies the problem of extending a processor with new features without weakening the security of the isolation mechanisms that the processor offers. We propose to use full abstraction as a formal criterion for the security of a processor extension, and we instantiate that criterion to the concrete case of extending a microprocessor that supports enclaved execution with secure interruptibility of these enclaves. This is a very relevant instantiation as several recent papers have shown that interruptibility of enclaves leads to a variety of software-based side-channel attacks. We propose a design for interruptible enclaves, and prove that it satisfies our security criterion. We also implement the design on an open-source enclave-enabled microprocessor, and evaluate the cost of our design in terms of performance and hardware size. △ Less

Submitted 29 January, 2020; originally announced January 2020.

Comments: Extended version of the paper "Provably Secure Isolation for Interruptible Enclaved Execution on Small Microprocessors"

A minimal core calculus for Solidity contracts

Authors: Massimo Bartoletti, Letterio Galletta, Maurizio Murgia

Abstract: The Ethereum platform supports the decentralized execution of smart contracts, i.e. computer programs that transfer digital assets between users. The most common language used to develop these contracts is Solidity, a Javascript-like language which compiles into EVM bytecode, the language actually executed by Ethereum nodes. While much research has addressed the formalisation of the semantics of E… ▽ More The Ethereum platform supports the decentralized execution of smart contracts, i.e. computer programs that transfer digital assets between users. The most common language used to develop these contracts is Solidity, a Javascript-like language which compiles into EVM bytecode, the language actually executed by Ethereum nodes. While much research has addressed the formalisation of the semantics of EVM bytecode, relatively little attention has been devoted to that of Solidity. In this paper we propose a minimal calculus for Solidity contracts, which extends an imperative core with a single primitive to transfer currency and invoke contract procedures. We build upon this formalisation to give semantics to the Ethereum blockchain. We show our calculus expressive enough to reason about some typical quirks of Solidity, like e.g. re-entrancy. △ Less

Submitted 6 August, 2019; originally announced August 2019.

Comments: arXiv admin note: substantial text overlap with arXiv:1905.04366

A true concurrent model of smart contracts executions

Authors: Massimo Bartoletti, Letterio Galletta, Maurizio Murgia

Abstract: The development of blockchain technologies has enabled the trustless execution of so-called smart contracts, i.e. programs that regulate the exchange of assets (e.g., cryptocurrency) between users. In a decentralized blockchain, the state of smart contracts is collaboratively maintained by a peer-to-peer network of mutually untrusted nodes, which collect from users a set of transactions (represent… ▽ More The development of blockchain technologies has enabled the trustless execution of so-called smart contracts, i.e. programs that regulate the exchange of assets (e.g., cryptocurrency) between users. In a decentralized blockchain, the state of smart contracts is collaboratively maintained by a peer-to-peer network of mutually untrusted nodes, which collect from users a set of transactions (representing the required actions on contracts), and execute them in some order. Once this sequence of transactions is appended to the blockchain, the other nodes validate it, re-executing the transactions in the same order. The serial execution of transactions does not take advantage of the multi-core architecture of modern processors, so contributing to limit the throughput. In this paper we propose a true concurrent model of smart contract execution. Based on this, we show how static analysis of smart contracts can be exploited to parallelize the execution of transactions. △ Less

Submitted 27 April, 2020; v1 submitted 10 May, 2019; originally announced May 2019.

Comments: Full version of the paper presented at COORDINATION 2020

Translation Validation for Security Properties

Authors: Matteo Busi, Pierpaolo Degano, Letterio Galletta

Abstract: Secure compilation aims to build compilation chains that preserve security properties when translating programs from a source to a target language. Recent research led to the definition of secure compilation principles that, if met, guarantee that the compilation chain in hand never violates specific families of security properties. Still, to the best of our knowledge, no effective procedure is av… ▽ More Secure compilation aims to build compilation chains that preserve security properties when translating programs from a source to a target language. Recent research led to the definition of secure compilation principles that, if met, guarantee that the compilation chain in hand never violates specific families of security properties. Still, to the best of our knowledge, no effective procedure is available to check if a compilation chain meets such requirements. Here, we outline our ongoing research inspired by translation validation, to effectively check one of those principles. △ Less

Submitted 15 January, 2019; originally announced January 2019.

Comments: Presented at PriSC Workshop 2019

Using Standard Typing Algorithms Incrementally

Authors: Matteo Busi, Pierpaolo Degano, Letterio Galletta

Abstract: Modern languages are equipped with static type checking/inference that helps programmers to keep a clean programming style and to reduce errors. However, the ever-growing size of programs and their continuous evolution require building fast and efficient analysers. A promising solution is incrementality, so one only re-types those parts of the program that are new, rather than the entire codebase.… ▽ More Modern languages are equipped with static type checking/inference that helps programmers to keep a clean programming style and to reduce errors. However, the ever-growing size of programs and their continuous evolution require building fast and efficient analysers. A promising solution is incrementality, so one only re-types those parts of the program that are new, rather than the entire codebase. We propose an algorithmic schema driving the definition of an incremental typing algorithm that exploits the existing, standard ones with no changes. Ours is a grey-box approach, meaning that just the shape of the input, that of the results and some domain-specific knowledge are needed to instantiate our schema. Here, we present the foundations of our approach and we show it at work to derive three different incremental typing algorithms. The first two implement type checking and inference for a functional language. The last one type-checks an imperative language to detect information flow and non-interference. We assessed our proposal on a prototypical implementation of an incremental type checker. Our experiments show that using the type checker incrementally is (almost) always rewarding. △ Less

Submitted 27 November, 2018; v1 submitted 1 August, 2018; originally announced August 2018.

Comments: corrected and updated; experimental results added

Tool Supported Analysis of IoT

Authors: Chiara Bodei, Pierpaolo Degano, Letterio Galletta, Emilio Tuosto

Abstract: The design of IoT systems could benefit from the combination of two different analyses. We perform a first analysis to approximate how data flow across the system components, while the second analysis checks their communication soundness. We show how the combination of these two analyses yields further benefits hardly achievable by separately using each of them. We exploit two independently devel… ▽ More The design of IoT systems could benefit from the combination of two different analyses. We perform a first analysis to approximate how data flow across the system components, while the second analysis checks their communication soundness. We show how the combination of these two analyses yields further benefits hardly achievable by separately using each of them. We exploit two independently developed tools for the analyses. Firstly, we specify IoT systems in IoT-LySa, a simple specification language featuring asynchronous multicast communication of tuples. The values carried by the tuples are drawn from a term-algebra obtained by a parametric signature. The analysis of communication soundness is supported by ChorGram, a tool developed to verify the compatibility of communicating finite-state machines. In order to combine the analyses we implement an encoding of IoT-LySa processes into communicating machines. This encoding is not completely straightforward because IoT-LySa has multicast communications with data, while communication machines are based on point-to-point communications where only finitely many symbols can be exchanged. To highlight the benefits of our approach we appeal to a simple yet illustrative example. △ Less

Submitted 29 November, 2017; originally announced November 2017.

Comments: In Proceedings ICE 2017, arXiv:1711.10708

Journal ref: EPTCS 261, 2017, pp. 37-56

Tracing where IoT data are collected and aggregated

Authors: Chiara Bodei, Pierpaolo Degano, Gian-Luigi Ferrari, Letterio Galletta

Abstract: 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 addres… ▽ More 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. △ Less

Submitted 18 July, 2017; v1 submitted 26 October, 2016; originally announced October 2016.

ACM Class: F.1.2; F.3.1

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 3 (July 19, 2017) lmcs:2186

A Step Towards Checking Security in IoT

Authors: Chiara Bodei, Pierpaolo Degano, Gian-Luigi Ferrari, Letterio Galletta

Abstract: 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. 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. △ Less

Submitted 10 August, 2016; originally announced August 2016.

Comments: In Proceedings ICE 2016, arXiv:1608.03131

ACM Class: F.3.2; D.2.4

Journal ref: EPTCS 223, 2016, pp. 128-142

Event-driven Adaptation in COP

Authors: Pierpaolo Degano, Gian-Luigi Ferrari, Letterio Galletta

Abstract: 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… ▽ More 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. △ Less

Submitted 19 June, 2016; originally announced June 2016.

Comments: In Proceedings PLACES 2016, arXiv:1606.05403

Journal ref: EPTCS 211, 2016, pp. 37-45

A Context-Oriented Extension of F#

Authors: Andrea Canciani, Pierpaolo Degano, Gian-Luigi Ferrari, Letterio Galletta

Abstract: 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… ▽ More 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#. △ Less

Submitted 23 December, 2015; originally announced December 2015.

Comments: In Proceedings FOCLASA 2015, arXiv:1512.06947

ACM Class: D.1.1; D.1.6; D.3.4

Journal ref: EPTCS 201, 2015, pp. 18-32

Typing Context-Dependent Behavioural Variation

Authors: Pierpaolo Degano, Gian-Luigi Ferrari, Letterio Galletta, Gianluca Mezzetti

Abstract: 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… ▽ More 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. △ Less

Submitted 26 February, 2013; originally announced February 2013.

Comments: In Proceedings PLACES 2012, arXiv:1302.5798

ACM Class: D.3.1; F.3.1; F.3.2

Journal ref: EPTCS 109, 2013, pp. 28-33

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

Authors: Letterio Galletta, Giorgio Levi

Abstract: 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 Couso… ▽ More 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. △ Less

Submitted 11 August, 2011; originally announced August 2011.

Comments: In Proceedings WWV 2011, arXiv:1108.2085

ACM Class: D.2.4; F.3.1; F.3.2

Journal ref: EPTCS 61, 2011, pp. 81-95