The Internet of Things (IoT) revolution is reshaping how physical devices embedded with software connect to the Internet, facilitating seamless data exchange and driving automation. Industrial IoT (IIoT) extends these capabilities to industrial devices and Cyber-Physical Systems (CPS), driving Intelligent Manufacturing. This integration supports advanced applications like remote monitoring, predictive maintenance, machine learning (ML), and artificial intelligence (AI) optimization, enhancing production efficiency, adaptability, and decisionmaking. However, managing the vast amounts of data generated requires scalable, automated software architectures. Many small and medium-sized enterprises (SME) face challenges in building such systems due to limited resources and expertise, often starting with manual data collection and basic automation.This paper presents a solution: a fully automated, configurable, and scalable software architecture for Intelligent Manufacturing. Our system has been operational for almost one and a half years on 21 plants, processing about 17K tasks, amounting to more than three months of computations. The experimental results show that automation and elasticity have been needed by such systems since the beginning, while scalability is not required during an initial experimentation phase.

Hyperledger Fabric (HF) is currently the one that made blockchain and smart contracts accessible to industries, providing highly customizable solutions for many enterprise use cases. Despite this, programmers are often discouraged from implementing smart contracts due to the high learning curve and security risks of naive smart contract implementations. At the same time, the advent of Large Language Models (LLMs) for code generation led to new possible scenarios such as creating new smart contract applications starting from natural language, allowing to reduce costs and development times. This paper investigates the maturity of LLMs for the code generation of HF smart contracts. In particular, we (i) generate smart contracts written in Go for HF starting from natural language descriptions, (ii) select state-of-the-art static analyzers of Go program, and (iii) perform a quality and security assessment of the generated smart contracts. Our empirical results show current LLMs do not produce high-quality smart contracts, and a relevant effort to debug and patch contracts containing bugs and possible vulnerabilities.

Sound static analysis allows one to overapproximate all possible program executions to infer various properties. However, it requires quite some effort to formalize and prove the soundness of program semantics. Most software applications developed nowadays are distributed systems in which different [micro]services communicate through synchronous and asynchronous mechanisms. These applications are composed of programs developed in many programming languages and rely on many technologies. However, sound static analysis might be particularly promising in distributed architectures, where exhaustively (or even partially) testing such systems is often prohibitive. This paper presents our ongoing work on applying LiSA (Library for Static Analysis) to microservices. So far, our effort has focused on one programming language (Python), a few libraries (ROS2, pika, FastAPI, Django), and the architectural reconstruction of distributed applications. However, it already shows some promising results and general patterns that might be followed to develop such analyses.

Cybersecurity in mission-critical robotic applications is a necessity to scale deployments securely. ROS2 builds upon DDS-Security specs in ROS Client Library (RCL) to implement its security features. Utilizing SROS2, developers have access to a set of utilities to help set up security in a way RCL can use. Through SROS2, security deployment is eased for developers. However, while access control is handled by DDS and consequently based on the SROS2-generated permission artifacts, the necessary authorization policies are manually generated by developers. This requires an entire system exercise to be sampled via live extraction and, per each node, list all the necessary Topics, Services, and Actions, which is a daunting and laborious process. Developers first have to generate tests. Then, they obtain a ’snapshot’ of the system for each test. Later, these snapshots must be collected and grouped into a policy by a minimum set of rules. All this procedure is quite error-prone. This paper introduces LiSA4ROS2, a tool for automatically extract the ROS2 computational graph via static analysis to derive a minimal correct configuration for ROS2 security policies. Our approach relies on the abstract interpretation theory to statically overapproximate all possible executions to extract a minimal and complete configuration per node. We evaluate our approach with minimal examples covering all the main communication patterns in ROS2 tutorials and all publicly available real-world ROS2 Python systems extracted from GitHub. The results of the minimal examples show that LiSA4ROS2 precisely supports all the main communication patterns. The extensive evaluation underlines that our prototype implementation of the analysis in LiSA4ROS2 is already able to precisely analyze 66% of existing repositories, automatically producing detailed computational graphs and access policies. All the results of the analysis, as well as a Docker artifact to reproduce them, are publicly available.

Abstract In this paper, we introduce Tarsis, a new abstract domain based on the abstract interpretation theory that approximates string values through finite state automata. The main novelty of Tarsis is that it works over an alphabet of strings instead of single characters. On the one hand, such an approach requires a more complex and refined definition of the lattice operators and of the abstract semantics of string operators. On the other hand, it is in position to obtain strictly more precise results than state‐of‐the‐art approaches. We compare Tarsis both with simpler domains and with the standard automata model, targeting case studies containing standard yet challenging string manipulations. The performance gain w.r.t. the standard automata model is also assessed, measuring the speed‐up gained by Tarsis. Experiments confirm that Tarsis can obtain precise results without incurring in excessive computational costs.

Software verification aims to prove that a program satisfies some given properties for all its possible executions. Software evolved incredibly fast during the last century, exposing several challenges to this scientific discipline. The goal of the “Challenges of Software Verification Symposium” is to monitor the state-of-the-art in this field. In this article, we will present the evolution of software from its inception in the 1940s to today’s applications, how this exposed new challenges to software verification, and what this discipline achieved. We will then discuss how this chapter covers most of the current open challenges, the possible future software developments, and what challenges this will raise in software verification.

Robot Operating System 2 (ROS 2) is the de-facto standard framework for developing distributed robotic applications. However, ensuring the correctness and security of these applications remains a significant challenge. This paper presents a novel approach to statically analyze ROS 2 applications using abstract interpretation. By extracting the architecture graph of the application, our method derives minimal access control policies that can be used to leverage security. We implemented our approach using the Library for Static Analysis (LiSA), providing a toolset that facilitates the development of sound static analyzers for ROS 2. The results demonstrate the effectiveness of our approach in enhancing the security of ROS 2 applications.

Machine learning has proved invaluable for a range of different tasks, yet it also proved vulnerable to evasion attacks, i.e., maliciously crafted perturbations of inputs designed to force mispredictions. In this article we propose a novel technique to certify the security of machine learning models against evasion attacks with respect to an expressive threat model, where the attacker can be represented by an arbitrary imperative program. Our approach is based on a transformation of the model under attack into an equivalent imperative program, which is then analyzed using the traditional abstract interpretation framework. This solution is sound, efficient and general enough to be applied to a range of different models, including decision trees, logistic regression and neural networks. Our experiments on publicly available datasets show that our technique yields only a minimal number of false positives and scales up to cases which are intractable for a competitor approach.

Software security vulnerabilities and leakages of private information are two of the main issues in modern software systems. Several different approaches, ranging from design techniques to run-time monitoring, have been applied to prevent, detect and isolate such vulnerabilities. Static taint analysis has been particularly successful in detecting injection vulnerabilities at compile time. However, its extension to detect leakages of sensitive data has been only partially investigated. In this paper, we introduce BackFlow, a backward flow reconstructor that, starting from the results of a generic taint analysis engine, reconstructs the flow of tainted data. If successful, BackFlow provides full information about the flow that such data (e.g. private information or user input) traversed inside the program before reaching a sensitive point (e.g. Internet communication or execution of an SQL query). Such information is needed to extend taint analysis to privacy analyses, since in such a scenario it is important to know which exact type of sensitive data flows to what type of communication channels. BackFlow has been implemented in Julia (an industrial static analyzer for Java, Android and .NET programs), and applied to WebGoat and different benchmarks to detect both injections and privacy issues. The experimental results prove that BackFlow is able to reconstruct the flow of tainted data for most of the true positives, it scales up to industrial applications, and it can be effectively applied to privacy analysis, such as the detection of sensitive data leaks or compliance with a data regulation.

Abstract The Open Web Application Security Project (OWASP), released the “OWASP Top 10 Internet of Things 2018” list of the high-priority security vulnerabilities for IoT systems. The diversity of these vulnerabilities poses a great challenge toward development of a robust solution for their detection and mitigation. In this paper, we discuss the relationship between these vulnerabilities and the ones listed by OWASP Top 10 (focused on Web applications rather than IoT systems), how these vulnerabilities can actually be exploited, and in which cases static analysis can help in preventing them. Then, we present an extension of an industrial analyzer (Julia) that already covers five out of the top seven vulnerabilities of OWASP Top 10, and we discuss which IoT Top 10 vulnerabilities might be detected by the existing analyses or their extension. The experimental results present the application of some existing Julia’s analyses and their extension to IoT systems, showing its effectiveness of the analysis of some representative case studies.

A formal translation of CIL (i.e., .Net) bytecode into Java bytecode is introduced and proved sound with respect to the language semantics. The resulting code is then analyzed with Julia, an industrial static analyzer of Java bytecode. The overall process of translation and analysis is fast, scales to industrial programs, and introduces a negligible number of false alarms. The main contribution of this work is to leverage existing, mature, and sound analyzers for Java bytecode by applying them also to the wide range of .Net software systems. Experimental results show the actual effectiveness of this approach when applied to all the system libraries of the Microsoft .Net framework version 4.0.30319 (about 5 MLOCs).

Summary Smartphone and automotive technologies are rapidly converging, letting drivers enjoy communication and infotainment facilities and monitor in‐vehicle functionalities, via on‐board diagnostics (OBD) technology. Among the various automotive apps available in playstores, Android Auto infotainment and OBD‐II apps are widely used and are the most popular choice for smartphone to car interaction. Automotive apps have the potential of turning cars into smartphones on wheels but can be also the gateway of attacks. This paper defines a static analysis that identifies potential security risks in Android infotainment and OBD‐II apps. It identifies a set of potential security threats and presents an actual static analyzer for such apps. It has been applied to most of the highly rated infotainment apps available in the Google Play store, as well as on the available open‐source OBD‐II apps, against a set of possible exposure scenarios. Results show that almost 60% of such apps are potentially vulnerable and that 25% pose security threats related to the execution of JavaScript. The analysis of the OBD‐II apps shows possibilities of severe controller area network injections and privacy violations, because of leaks of sensitive information.

The most dangerous security-related software errors, according to the OWASP Top Ten 2017 list, affect web applications. They are potential injection attacks that exploit user-provided data to execute undesired operations: database access and updates ( SQL injection ); generation of malicious web pages ( cross-site scripting injection ); redirection to user-specified web pages ( redirect injection ); execution of OS commands and arbitrary scripts ( command injection ); loading of user-specified, possibly heavy or dangerous classes at run time ( reflection injection ); access to arbitrary files on the file system ( path-traversal ); and storing user-provided data into heap regions normally assumed to be shielded from the outside world ( trust boundary violation ). All these attacks exploit the same weakness: unconstrained propagation of data from sources that the user of a web application controls into sinks whose activation might trigger dangerous operations. Although web applications are written in a variety of languages, Java remains a frequent choice, in particular for banking applications, where security has tangible relevance. This article defines a unified, sound protection mechanism against such attacks, based on the identification of all possible explicit flows of tainted data in Java code. Such flows can be arbitrarily complex, passing through dynamically allocated data structures in the heap. The analysis is based on abstract interpretation and is interprocedural, flow-sensitive, and context-sensitive. Its notion of taint applies to reference (non-primitive) types dynamically allocated in the heap and is object-sensitive and field-sensitive. The analysis works by translating the program into Boolean formulas that model all possible data flows. Its implementation, within the Julia analyzer for Java and Android, found injection security vulnerabilities in the Internet banking service and in the customer relationship management of large Italian banks, as well as in a set of open-source third-party applications. It found the command injection, which is at the origin of the 2017 Equifax data breach, one of the worst data breaches ever. For objective, repeatable results, this article also evaluates the implementation on two open-source security benchmarks: the Juliet Suite and the OWASP Benchmark for the automatic comparison of static analyzers for cybersecurity. We compared this technique against more than 10 other static analyzers, both free and commercial. The result of these experiments is that ours is the only analysis for injection that is sound (up to well-stated limitations such as multithreading and native code) and works on industrial code, and it is also much more precise than other tools.

With over 2 billion active mobile users and a large array of features, Android is the most popular operating system for mobile devices. Android Auto allows such devices to connect with an in-car compatible infotainment system, and it became a popular choice as well. However, as the trend for connecting car dashboard to the Internet or other devices grows, so does the potential for security threats. In this paper, a set of potential security threats are identified, and a static analyzer for the Android Auto infotainment system is presented. All the infotainment apps available in Google Play Store have been checked against that list of possible exposure scenarios. Results show that almost 80% of the apps are potentially vulnerable, out of which 25% poses security threats related to execution of JavaScript.

Although Information Foraging Theory (IFT) research for desktop environments has provided important insights into numerous information foraging tasks, we have been unable to locate IFT research for mobile environments. Despite the limits of mobile platforms, mobile apps are increasingly serving functions that were once exclusively the territory of desktops - and as the complexity of mobile apps increases, so does the need for foraging. In this paper we investigate, through a theory-based, dual replication study, whether and how foraging results from a desktop IDE generalize to a functionally similar mobile IDE. Our results show ways prior foraging research results from desktop IDEs generalize to mobile IDEs and ways they do not, and point to challenging open research questions for foraging on mobile environments.

Mobile devices are rich in sensors, such as a Global Positioning System (GPS) tracker, microphone and camera, and have access to numerous sources of personal information, including the device ID, contacts and social data. This richness increases the functionality of mobile apps, but also creates privacy threats. As a result, different solutions have been proposed to verify or enforce privacy policies. A key limitation of existing approaches is that they reason about privacy at a coarse level, without accounting for declassification rules, such that the location for instance is treated as a single unit of information without reference to its many fields. As a result, legitimate app behaviors --- such as releasing the user's city rather than exact address --- are perceived as privacy violations, rendering existing analyses overly conservative and thus of limited usability.

Given a program whose functionality depends on access to certain external resources, we investigate the question of how to gracefully degrade functionality when a subset of those resources is unavailable. The concrete setting motivating this problem statement is mobile applications, which rely on contextual data (e.g., device identifiers, user location and contacts, etc.) to fulfill their functionality. In particular, we focus on the Android platform, which mediates access to resources via an installation-time permission model. On the one hand, granting an app the permission to access a resource (e.g., the device ID) entails privacy threats (e.g., releasing the device ID to advertising servers). On the other hand, denying access to a resource could render the app useless (e.g., if inability to read the device ID is treated as an error state). Our goal is to specialize an existing Android app in such a way that it is disabled from accessing certain sensitive resources (or contextual data) as specified by the user, while still being able to execute functionality that does not depend on those resources. We present ShamDroid, a program transformation algorithm, based on specialized forms of program slicing, backwards static analysis and constraint solving, that enables the use of Android apps with partial permissions. We rigorously state the guarantees provided by ShamDroid w.r.t. functionality maximization. We provide an evaluation over the top 500 Google Play apps and report on an extensive comparative evaluation of ShamDroid against three other state-of-the-art solutions (APM, XPrivacy, and Google App Ops) that mediate resource access at the system (rather than app) level. ShamDroid performs better than all of these tools by a significant margin, leading to abnormal behavior in only 1 out of 27 apps we manually investigated, compared to the other solutions, which cause crashes and abnormalities in 9 or more of the apps. This demonstrates the importance of performing app-sensitive mocking.

SUMMARY Strings are widely used in modern programming languages in various scenarios. For instance, strings are used to build up Structured Query Language (SQL) queries that are then executed. Malformed strings may lead to subtle bugs, as well as non‐sanitized strings may raise security issues in an application. For these reasons, the application of static analysis to compute safety properties over string values at compile time is particularly appealing. In this article, we propose a generic approach for the static analysis of string values based on abstract interpretation. In particular, we design a suite of abstract semantics for strings, where each abstract domain tracks a different kind of information. We discuss the trade‐off between efficiency and accuracy when using such domains to catch the properties of interest. In this way, the analysis can be tuned at different levels of precision and efficiency, and it can address specific properties.Copyright © 2013 John Wiley & Sons, Ltd.

This paper addresses the problem of detecting JavaScript security vulnerabilities in the client side of Web applications. Such vulnerabilities are becoming a source of growing concern due to the rapid migration of server-side business logic to the client side, combined with new JavaScript-backed Web technologies, such as AJAX and HTML5. Detection of client-side vulnerabilities is challenging given the dynamic and event-driven nature of JavaScript. We present a hybrid form of JavaScript analysis, which augments static analysis with (semi-)concrete information by applying partial evaluation to JavaScript functions according to dynamic data recorded by the Web crawler. The dynamic component rewrites the program per the enclosing HTML environment, and the static component then explores all possible behaviors of the partially evaluated program (while treating user-controlled aspects of the environment conservatively).

Mobile app markets have lowered the barrier to market entry for software producers. As a consequence, an increasing number of independent app developers offer their products, and recent platforms such as the MIT App Inventor and Microsoft's TouchDevelop enable even lay programmers to develop apps and distribute them in app markets.

SUMMARY In this paper, we present heckmate, the first generic static analyzer of multithreaded Java programs based on abstract interpretation. heckmate can be tuned at different levels of precision and efficiency in order to prove various properties (e.g., absence of divisions by zero and data races), and it is sound for multithreaded programs. It supports all the most relevant features of Java multithreading, such as dynamic thread creation, runtime creation of monitors, and dynamic allocation of memory. The experimental results demonstrate that heckmate is accurate and efficient enough to analyze programs with some thousands of statements and a potentially infinite number of threads. Copyright © 2012 John Wiley & Sons, Ltd.

In this paper we present Checkmate, a generic static analyzer of Java multithreaded programs based on the abstract interpretation theory. It supports all the most relevant features of Java multithreading, as dynamic unbounded thread creation, runtime creation of monitors, and dynamic allocation of shared memory. We implement a wide set of properties, from the ones interesting also for sequential programs, e.g. division by zero, to the ones typical of multithtreaded programs, e.g. data races. We analyze several external case studies and benchmarks with Checkmate, and we study the experimental results both in term of precision and efficiency. It turns out that the analysis is particularly accurate and we are in position to analyze programs composed by some thousands of statements and a potentially infinite number of threads. As far as we know, Checkmate is the first generic static analyzer of Java multithreaded programs.

The.NET intermediate language (MSIL) allows expressing both statically verifiable memory and type safe code (typi-cally called managed), as well as unsafe code using direct pointer manipulations. Unsafe code can be expressed in C# by marking regions of code as unsafe. Writing unsafe code can be useful where the rules of managed code are too strict. The obvious drawback of unsafe code is that it opens the door to programming errors typical of C and C++, namely memory access errors such as buffer overruns. Worse, a sin-gle piece of unsafe code may corrupt memory and destabi-lize the entire runtime or allow attackers to compromise the security of the platform. We present a new static analysis based on abstract in-terpretation to check memory safety for unsafe code in the.NET framework. The core of the analysis is a new numeri-cal abstract domain, Strp, which is used to efficiently com-pute memory invariants. Strp is combined with lightweight abstract domains to raise the precision, yet achieving scala-bility. We implemented this analysis in Clousot, a generic static analyzer for.NET. In combination with contracts ex-pressed in FoxTrot, an MSIL based annotation language for.NET, our analysis provides static safety guarantees on memory accesses in unsafe code. We tested it on all the as-semblies of the.NET framework. We compare our results with those obtained using existing domains, showing how they are either too imprecise (e.g., Intervals or Octagons) or too expensive (Polyhedra) to be used in practice.

Threads communicate implicitly through shared memory. Because of the random interleaving during their parallel execution, nondeterministic behaviors possibly arise that is why multithreaded programming is strictly more difficult than programming in sequential languages. Moreover the random interleaving may lead to subtle bugs, that are really hard to be detected and fixed. We propose a novel deterministic property focused on multithreading. We define it as difference among concrete traces, and then we abstract it in two separate steps in order to statically analyze it. At the intermediate level of abstraction, we propose the new idea of weak determinism. We sketch how the proposed property may be used in order to semi-automatically parallelize sequential programs. Finally, we present some experimental results when applying the analysis to a set of well-known benchmarks. We believe that our approach, dealing directly with the source of the problem (i.e. the nondeterministic interactions via shared memory) is in position to bypass the actual limits of the static analysis of multithreaded programs, mostly focused on properties like data race condition and absence of deadlocks.