Abstract Event-driven programming provides a natural fit for the reactive nature of pervasive systems like the Internet of Things (IoT) and Collective Adaptive Systems (CASs). Attribute-based memory Updates (AbU) is a calculus based on Event-Condition-Action (ECA) rules, well-suited for modeling such decentralized systems. This paper introduces a novel extension of AbU by incorporating ECA rule priorities . We show how this extension facilitates the natural expression of prioritized behaviors and enables the implementation of distributed data structures like Conflict-free Replicated Data Types (CRDTs). Furthermore, by leveraging the local invariants of AbU nodes and priorities we address the problem of enforcing global invariants in order to enhance the reliability and predictability of CASs. This is achieved through a syntactic transformation that projects global invariants into local ones and introduces high-priority synchronization rules, so that system-level properties can be guaranteed without relying on a central authority.

In modern computing systems, preventing sensitive information leakage is a crucial issue. Indeed, to deploy secure computing systems, data protection is an aspect that cannot be ignored. Many security requirements are adopted in this respect, such as opacity and non-interference . The first assures that the truth value of a predicate is masked during computation, while the second prevents confidential information is leaked through uncontrolled system components. Unfortunately, despite their simple intended meaning, confidentiality notions are quite difficult requirements to enforce. In fact, they are actually hyperproperties , and thus require enforcing mechanisms that reason on multiple executions at a time. To develop effective verification and validation mechanisms for confidentiality notions, it is crucial to precisely characterize the requirements of system executions they dictate. In this article, we investigate the relation between abstract non-interference (a weakening of non-interference observing properties of data instead of concrete values) and opacity through the lens of abstract interpretation . By adopting such a holistic, abstract approach, we show how to formally characterize the structure of confidentiality notions and to compare them in terms of the constraints on system executions they impose and verification complexity. In addition, we show how code obfuscation can be restated as a confidentiality problem by defining a corresponding confidentiality notion that can possibly be enforced. Finally, by exploiting the recently proposed static analysis approach for verifying non-interference, based on hypersemantics , we show how to verify abstract non-interference, therefore opacity and other security requirements. Based on abstract interpretation , this yields an effective mechanism to enforce a broad range of confidentiality notions.

As the software engineering research community continues to propose novel approaches to automated test case generation for REST APIs, researchers face the labor-intensive task of empirically validating their methodologies and comparing them with the state-of-the-art. This process requires assembling a benchmark of case studies (notoriously difficult to find in the context of REST API testing), building and running each API, gathering competitor tools, conducting experimental testing sessions to collect effectiveness and efficiency metrics, and processing the results. These extensive engineering efforts consume time that could be otherwise spent on more research-oriented tasks. This paper introduces RESTgym, a flexible empirical infrastructure designed to assess the performance of REST API testing tools and facilitate comparative analysis with state-of-the-art approaches. By providing a standardized environment for comparison (currently consisting of 11 benchmark APIs and 6 state-of-the-art tools packed into containers, but easily extensible to add new APIs and tools) and an orchestration engine, RESTgym significantly reduces the time and effort required for researchers to evaluate REST API testing methodologies. The paper details the architecture and components of RESTgym and demonstrates its utility through a practical example, highlighting its potential to speed up research and development in automatedREST API testing. Video:http://tiny.cc/restgym-video

Hyperproperties are used to define correctness requirements that involve relations between multiple program executions. This allows, for instance, to model security and concurrency requirements, which cannot be expressed by means of trace properties.

Automatically crafting test scenarios for REST APIs helps deliver more reliable and trustworthy web-oriented systems. However, current black-box testing approaches rely heavily on the information available in the API's formal documentation, i.e., the Open API Specification (OAS for short). While useful, the OAS mostly covers syntactic aspects of the API (e.g., producer-consumer relations between operations, input value properties, and additional constraints in natural language), and it lacks a deeper understanding of the API business logic. Missing semantics include implicit ordering (logic dependency) between operations and implicit input-value constraints. These limitations hinder the ability of black-box testing tools to generate truly effective test cases automatically.

Attribute-based memory Updates (in short) is an interaction mechanism recently introduced for adapting the Event-Condition-Action (ECA) programming paradigm to distributed reactive systems, such as autonomic and smart IoT device ensembles. In this model, an event (e.g., an input from a sensor, or a device state update) can trigger an ECA rule, whose execution can cause the state update of (possibly) many remote devices at once; the latter are selected “on the fly” by means of predicates over their state, without the need of a central coordinating entity. However, the combination of different systems may yield unexpected interactions, e.g., when a new device is added to an existing secure system, potentially hindering the security of the whole ensemble of devices. This can be critical in the IoT, where smart devices are more and more pervasive in our daily life. In this paper, we consider the problem of ensuring security and safety requirements for systems (and, in turn, for IoT devices). The first are a form of noninterference, as they correspond to avoid forbidden information flows (e.g., information flows violating confidentiality); while the second are a form of non-interaction, as they correspond to avoid unintended executions (e.g., leading to erroneous/unsafe states). In order to formally model these requirements, we introduce suitable behavioral equivalences for . These equivalences are generalizations of hiding bisimilarity, i.e., a kind of weak bisimilarity where we can compare systems up-to actions at different levels of security. Leveraging these behavioral equivalences, we propose (syntactic) sufficient conditions guaranteeing the requirements and, then, effective algorithms for statically verifying such conditions.

Mass assignment is one of the most prominent vulnerabilities in RESTful APIs that originates from a misconfiguration in common web frameworks. This allows attackers to exploit naming convention and automatic binding to craft malicious requests that (massively) override data supposed to be read-only. In this paper, we adopt a black-box testing perspective to automatically detect mass assignment vulnerabilities in RESTful APIs. Indeed, execution scenarios are generated purely based on the OpenAPI specification, that lists the available operations and their message format. Clustering is used to group similar operations and reveal read-only fields, the latter are candidates for mass assignment. Then, test interaction sequences are automatically generated by instantiating abstract testing templates, with the aim of trying to use the found read-only fields to carry out a mass assignment attack. Test interactions are run, and their execution is assessed by a specific oracle, in order to reveal whether the vulnerability could be successfully exploited. The proposed novel approach has been implemented and evaluated on a set of case studies written in different programming languages. The evaluation highlights that the approach is quite effective in detecting seeded vulnerabilities, with a remarkably high accuracy.

RESTful services are commonly documented using OpenAPI specifications. Although numerous automated testing techniques have been proposed that leverage the machine-readable part of these specifications to guide test generation, their human-readable part has been mostly neglected. This is a missed opportunity, as natural language descriptions in the specifications often contain relevant information, including example values and inter-parameter dependencies, that can be used to improve test generation. In this spirit, we propose NLPtoREST, an automated approach that applies natural language processing techniques to assist REST API testing. Given an API and its specification, NLPtoREST extracts additional OpenAPI rules from the human-readable part of the specification. It then enhances the original specification by adding these rules to it. Testing tools can transparently use the enhanced specification to perform better test case generation. Because rule extraction can be inaccurate, due to either the intrinsic ambiguity of natural language or mismatches between documentation and implementation, NLPtoREST also incorporates a validation step aimed at eliminating spurious rules. We performed studies to assess the effectiveness of our rule extraction and validation approach, and the impact of enhanced specifications on the performance of eight state-of-the-art REST API testing tools. Our results are encouraging and show that NLPtoREST can extract many relevant rules with high accuracy, which can in turn significantly improve testing tools’ performance.

The immutable nature of Ethereum transactions, and consequently Ethereum smart-contracts, has stimulated the proliferation of many approaches aiming at detecting defects and security issues before the deployment of smart-contracts on the blockchain. Indeed, the actions performed by smart-contracts instantiated on the blockchain, possibly involving substantial financial value, cannot be undone. Unfortunately, smart-contracts source code is not always available, hence approaches based on static analysis have very often to face the problem of inspecting the compiled Ethereum Virtual Machine (EVM) bytecode, retrieved directly from the blockchain. However, due to the intrinsic complexity of EVM bytecode (especially in jumps address resolution), the state-of-the-art static analysis-based solutions have poor accuracy in the automated detection of Ethereum smart-contracts programming defects and vulnerabilities. This paper presents a novel approach based on symbolic execution of the EVM operands stack that allows to resolve jumps address in the EVM bytecode and to construct a precise Control-Flow Graph (CFG) of compiled smart-contracts. Many static analysis techniques are based on a CFG-based representation of the smart-contract to validate, and would therefore benefit from our approach. We have implemented the CFG reconstruction algorithm in a tool called EtherSolve . Then, we have validated the tool on a large dataset of real-world Ethereum smart-contracts, showing that EtherSolve extracts more precise CFGs, w.r.t. state-of-the-art available approaches. Finally, we have extended EtherSolve with two detectors for two of the most prominent Ethereum smart-contracts vulnerabilities (Reentrancy and Tx.origin). Experimental results show that exploiting the proposed CFG reconstruction static analysis, leads to more accurate vulnerabilities detection, w.r.t. state-of-the-art security tools. Editor’s note: Open Science material was validated by the Journal of Systems and Software Open Science Board.

In recent years, event-driven programming languages, in particular those based on Event Condition Action (ECA) rules, have emerged as a promising paradigm for implementing ubiquitous and pervasive systems. These implementations are mostly centralized, where a single server (often in the cloud) collects and processes all the inputs from the environment. In fact, placing the computation on the nodes interacting with the environment requires suitable abstractions for effective communication and coordination of (possibly large) ensembles of these distributed components — abstractions that current ECA languages are still missing. To this end, in this paper we present AbU, a calculus for modeling and reasoning about ECA-based systems with attribute-based communication. The latter is an interaction model recently introduced for the coordination of (possibly large) families of nodes: communication is similar to broadcast but the actual receivers are selected on the spot, by means of predicates over nodes properties. Thus, the programmer can specify interactions between nodes in a declarative way, abstracting from details such as nodes identity, number, or even their existence, without the need for a central server: the computation is moved on the “edge”, thus improving reliability, scalability, privacy and security. After having defined syntax and formal semantics of AbU, we showcase its expressiveness by providing some example applications and the encoding of AbC, the archetypal calculus with attribute-based communication. Then, we focus on two key properties of reactive systems: stabilization (i.e., termination of internal steps) and confluence. For both these properties we provide formal semantic definition, sufficient syntactic conditions on AbU systems, and algorithms to statically check such conditions. Hence, AbU is both a basis for the formal analysis of event-driven architectures with attributed-based interaction, and a reference model for a full-fledged language for IoT and edge computing.

Over the past few years, several novel black-box testing approaches targeting RESTful APIs have been proposed. In order to assess their effectiveness, such testing strategies had to be implemented as a prototype tool and validated on empirical data. However, developing a testing tool is a time-consuming task, and reimplementing from scratch the same common basic features represents a waste of resources that causes a remarkable overhead in the "time to market" of research results.In this paper, we present RestTestGen, an extensible framework for implementing new automated black-box testing strategies for RESTful APIs. The framework provides a collection of commonly used components, such as a robust OpenAPI specification parser, dictionaries, input value generators, mutation operators, oracles, and others. Many of the provided components are customizable and extensible, enabling researchers and practitioners to quickly prototype, deploy, and evaluate their novel ideas. Additionally, the framework facilitates the development of novel black-box testing strategies by guiding researchers, by means of abstract components that explicitly identify those parts of the framework requiring a concrete implementation.As an adoption example, we show how we can implement nominal and error black-box testing strategies for RESTful APIs, by reusing primitives and features provided by the framework, and by concretely extending very few abstract components.RestTestGen is open-source, actively maintained, and publicly available on GitHub at https://github.com/SeUniVr/RestTestGen

Products and materials traceability is essential in modern manufacturing, where the production must meet certain standards that range from Quality Control (QC) to the quality of the used materials. In this environment, blockchain applications allow certifying data provenience and subsequent modification, offering trust and security along the entire supply chain. Nonetheless, the design and the development of such applications are usually performed manually and, thus, subject to errors.In this paper, we propose a methodology allowing to automatically generate smart contracts starting from a SysML model. This approach allows easing the integration of blockchain applications in a production system: by abstracting the implementations with models, it is possible to generate smart contracts for different blockchains, connecting to multiple production environments.We applied the proposed methodology on a real manufacturing system, assessing the quality of a case-study production.

Abstract RESTful APIs (or REST APIs for short) represent a mainstream approach to design and develop web APIs using the REpresentational State Transfer architectural style. Black‐box testing, which assumes only the access to the system under test with a specific interface, is the only viable option when white‐box testing is impracticable. This is the case for REST APIs: their source code is usually not (or just partially) available, or a white‐box analysis across many dynamically allocated distributed components (typical of a micro‐services architecture) is computationally challenging. This paper presentsRestTestGen, a novel black‐box approach to automatically generate test cases for REST APIs, based on their interface definition (an OpenAPI specification). Input values and requests are generated for each operation of the API under test with the twofold objective of testing nominal execution scenarios and error scenarios. Two distinct oracles are deployed to detect when test cases reveal implementation defects. While this approach is mainly targeting the research community, it is also of interest to developers because, as a black‐box approach, it is universally applicable across different programming languages, or in the case external (compiled only) libraries are used in a REST API. The validation of our approach has been performed on more than 100 of real‐world REST APIs, highlighting the effectiveness of the approach in revealing actual faults in already deployed services.

Test coverage is a standard measure used to evaluate the completeness of a test suite. Coverage is typically computed on source code, by assessing the extent of source code entities (e.g., statements, data dependencies, control dependencies) that are exercised when running test cases. When considering REST APIs, an alternative perspective to assess test suite completeness is with respect to the service definition. This paper presents Restats, a test coverage tool for REST APIs that supports eight state-of-the-art test coverage metrics with a black-box perspective, i.e., only relying on the OpenAPI interface specification of the REST API under test. In fact, metrics are computed by only observing the HTTP requests and responses occurring at testing time, and no access to source/compiled code of the REST API is required. These coverage metrics come in handy for: (i) developers and test engineers working at development and maintenance tasks; (ii) stakeholders and customers who want to evaluate the completeness of acceptance tests; (iii) researches interested in comparing different automated test case generation strategies. Restats GitHub repository: https://github.com/SeUniVr/restats Restats demo video: https://smarturl.it/restats-demo

In literature, we can find research tools to automatically generate test cases for RESTful APIs, addressing the specificity of this particular programming domain. However, no direct comparison of these tools is available to guide developers in deciding which tool best fits their REST API project.In this paper, we present the results of an empirical comparison of automated black-box test case generation approaches for REST APIs. We surveyed the available black-box testing tools that have been proposed in recent literature, finding four usable prototypes: RestTestGen, RESTler, bBOXRT and RESTest. We used these tools to generate test cases for 14 real-world REST services. Then, testing results have been analyzed and compared in terms of robustness (i.e., success rate) and test coverage.Among the considered tools, RESTler appears to be the most solid, able to successfully test all case studies (the other tools experienced crashes). Conversely, test cases generated by RestTestGen scored the highest coverage, suggesting that its testing strategy is the most effective in testing REST APIs.

IoT platforms enable users to connect various smart devices and online services via reactive apps running on the cloud. These apps, often developed by third-parties, perform simple computations on data triggered by external information sources and actuate the results of computations on external information sinks. Recent research shows that unintended or malicious interactions between the different (even benign) apps of a user can cause severe security and safety risks. These works leverage program analysis techniques to build tools for unveiling unexpected interference across apps for specific use cases. Despite these initial efforts, we are still lacking a semantic framework for understanding interactions between IoT apps. The question of what security policy cross-app interference embodies remains largely unexplored. This article proposes a semantic framework capturing the essence of cross-app interactions in IoT platforms. The framework generalizes and connects syntactic enforcement mechanisms to bisimulation-based notions of security, thus providing a baseline for formulating soundness criteria of these enforcement mechanisms. Specifically, we present a calculus that models the behavioral semantics of a system of apps executing concurrently, and use it to define desirable semantic policies targeting the security and safety of IoT apps. To demonstrate the usefulness of our framework, we define and implement static analyses for enforcing cross-app security and safety, and prove them sound with respect to our semantic conditions. We also leverage real-world apps to validate the practical benefits of our tools based on the proposed enforcement mechanisms.

IoT platforms enable users to connect various smart devices and online services via reactive apps running on the cloud. These apps, often developed by third-parties, perform simple computations on data triggered by external information sources and actuate the results of computation on external information sinks. Recent research shows that unintended or malicious interactions between the different (even benign) apps of a user can cause severe security and safety risks. These works leverage program analysis techniques to build tools for unveiling unexpected interference across apps for specific use cases. Despite these initial efforts, we are still lacking a semantic framework for understanding interactions between IoT apps. The question of what security policy cross-app interference embodies remains largely unexplored. This paper proposes a semantic framework capturing the essence of cross-app interactions in IoT platforms. The framework generalizes and connects syntactic enforcement mechanisms to bisimulation-based notions of security, thus providing a baseline for formulating soundness criteria of these enforcement mechanisms. Specifically, we present a calculus that models the behavioral semantics of a system of apps executing concurrently, and use it to define desirable semantic policies in the security and safety context of IoT apps. To demonstrate the usefulness of our framework, we define static mechanisms for enforcing cross-app security and safety, and prove them sound with respect to our semantic conditions. Finally, we leverage real-world apps to validate the practical benefits of our policy framework.

Software watermarking is a software protection technique used to defend the intellectual property of proprietary code. In particular, software watermarking aims at preventing software piracy by embedding a signature, i.e. an identifier reliably representing the owner, in the code. When an illegal copy is made, the owner can claim his/her identity by extracting the signature. It is important to hide the signature in the program in order to make it difficult for the attacker to detect, tamper or remove it. In this work, we present a formal framework for software watermarking, based on program semantics and abstract interpretation, where attackers are modelled as abstract interpreters. In this setting, we can prove that the ability to identify signatures can be modelled as a completeness property of the attackers in the abstract interpretation framework. Indeed, hiding a signature in the code corresponds to embed it as a semantic property that can be retrieved only by attackers that are complete for it. Any abstract interpreter that is not complete for the property specifying the signature cannot detect, tamper or remove it. We formalize in the proposed framework the major quality features of a software watermarking technique: secrecy, resilience, transparence and accuracy. This provides a unifying framework for interpreting both watermarking schemes and attacks, and it allows us to formally compare the quality of different watermarking techniques. Indeed, a large number of watermarking techniques exist in the literature and they are typically evaluated with respect to their secrecy, resilience, transparence and accuracy to attacks. Formally identifying the attacks for which a watermarking scheme is secret, resilient, transparent or accurate can be a complex and error-prone task, since attacks and watermarking schemes are typically defined in different settings and using different languages (e.g. program transformation vs. program analysis), complicating the task of comparing one against the others.