arXiv subjects

Letterio Galletta

Publications and source records attributed to Letterio Galletta.

At least 19 recordsLinked to original sources

arXiv2026

Enforcement of In-Kernel Stateful Security Policies via eBPF

Many attacks against workloads running on multi-tenant systems are multi-step and history-dependent: sequences of innocuous operations whose malicious nature emerges only over an execution trace. Defending against them requires security policies that are stateful, are enforced within the kernel, and have a precise semantics. Currently deployed proposals fail on at least one count: kernel's built-in syscall filtering and classical MAC frameworks are stateless, while current eBPF-based tools express their policies through ad hoc YAML rules that cannot capture temporal relations among events, and whose semantics is defined only by the implementation. We present BPFence, an in-kernel runtime-verification framework that satisfies the properties above. BPFence provides a policy language with a formal semantics that can express temporal relations among events. It also provides a type system that statically distinguishes events the kernel can control from those it can only observe. Every well-typed policy is compiled into a finite-state monitor proved correct with respect to its semantics, and then into eBPF programs that run inside the kernel. We evaluate BPFence on seven case studies drawn from real-world attack patterns, and on a set of micro- and macro-benchmarks to show that the enforcement overhead remains compatible with production deployment.

cs.CR↗

arXiv2026

A Unified Framework and Comparative Study of Decentralized Finance Derivatives Protocols

Decentralized Finance (DeFi) applications introduce novel financial instruments replicating and extending traditional ones through blockchain-based smart contracts. Among these applications, DeFi derivatives protocols enable the creation and trading of decentralized derivative instruments whose value depends on underlying cryptoassets, indices, or other reference variables. Despite their growing significance, however, they remain relatively understudied compared to other DeFi protocols, such as lending protocols and decentralized exchanges. This paper systematically analyzes DeFi derivatives protocols, categorized into perpetuals, options, and synthetics, with the aim of comparing their instrument structures, protocol mechanisms, operational dynamics, and economic agents. We provide a formal characterization of the main classes of decentralized derivative instruments and develop a protocol-agnostic framework that connects instrument-level specifications, market-state variables, and protocol-level mechanisms. We complement the analytical framework with numerical simulations that evaluate how derivative positions evolve under varying economic conditions, including changes in underlying asset prices, volatility, protocol-specific fees, and leverage. Overall, this study provides a structured analytical framework for understanding and comparing the design and functioning of decentralized finance derivatives protocols.

cs.GT↗

arXiv2026

Checking Information Flow in Cloud-based IoT Access Control Policies (Extended Version)

Many cloud providers for IoT technologies offer access control mechanisms whose proper configuration is critical for security. However, verifying permissions in isolation is insufficient in a setting where devices have different levels of trust or are compartmentalised in various subsystems. This work analyses IoT access control policies to identify potential security vulnerabilities from unwanted information flow between devices. To this end, we formally model AWS IoT Core's components and define an information flow graph to capture the communication among devices permitted by the access control policies. We build a finite representation of the graph by leveraging an SMT solver, thus enabling the verification of information flow between devices. We implement our approach in a tool called IOT:POKER, and assess it on a realistic scenario and several real-world policies.

cs.CR↗

arXiv2026

Policies for Fair Exchanges of Resources

People increasingly use digital platforms to exchange resources in accordance with 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.

cs.LO↗

arXiv2024

A Logic for Policy Based Resource Exchanges in Multiagent Systems

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.

cs.LO↗

arXiv2024

Explainable Ponzi Schemes Detection on Ethereum

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.

cs.CR↗

arXiv2022

Automatic Fair Exchanges

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.

cs.CR↗

arXiv2022

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

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.

cs.CR↗

arXiv2021

A theory of transaction parallelism in blockchains

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.

cs.CR↗

arXiv2020

Private-Yet-Verifiable Contact Tracing

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.

cs.CR↗

arXiv2020

A type language for message passing component-based systems

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.

cs.PL↗

arXiv2020

A true concurrent model of smart contracts executions

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.

cs.PL↗

arXiv2020

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

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.

cs.PL↗

arXiv2020

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

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.

cs.CR↗

arXiv2019

A minimal core calculus for Solidity contracts

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.

cs.PL↗

arXiv2019

Translation Validation for Security Properties

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.

cs.PL↗

arXiv2018

Using Standard Typing Algorithms Incrementally

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.

cs.PL↗

arXiv2017

Tool Supported Analysis of IoT

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.

cs.LO↗