Due to its interdisciplinary nature, the development of data science software is particularly prone to a wide range of potential mistakes that can easily and silently compromise the final results. Several tools have been proposed that can help the data scientist in identifying the most common, low-level programming issues. However, these tools often fall short in detecting higher-level, domain-specific issues typical of data science pipelines, where subtle errors may not trigger exceptions but can still lead to incorrect or misleading outcomes, or unexpected behaviors. In this paper, we present PYRA , a static analysis tool that aims at detecting code smells in data science workflows. PYRA builds upon the Abstract Interpretation framework to infer abstract datatypes, and exploits such information to flag 16 categories of potential code smells concerning misleading visualizations, challenges for reproducibility, as well as misleading, unreliable or unexpected results. Unlike traditional linters, which focus on syntactic or stylistic issues, PYRA reasons over a domain-specific type system to identify data science-specific problems – such as improper data preprocessing steps and procedures’ misapplications – that could silently propagate through a data-manipulation pipeline. Beyond static checking, we envision tools like PYRA becoming integral components of the development loop, with analysis reports guiding correction and helping assess the reliability of machine learning pipelines. We evaluate PYRA on a benchmark suite of real-world Jupyter notebooks, showing its effectiveness in detecting practical data science issues, thereby enhancing transparency, correctness, and reproducibility in data science software.

Unstructured (or, semi-structured) natural language is mostly used to capture the requirement specifications both for legacy software systems and for modern day software systems. The adoption of a formal approach to the specification of the requirements, using goal models, enables rigorous and formal inspections while analyzing the requirements for satisfiability, consistency, completeness, conflicts and ambiguities. However, such a formal approach is often considered burdening for the analysts’ activity as it requires additional skills, and is therefore, discarded a priori. This works aims to bridge the gap between natural language requirement specifications and efficient goal model analysis techniques. We propose a framework that uses extensive natural language processing techniques to transform a set of unstructured natural language requirement specifications to the corresponding goal model. We combine techniques such as parts-of-speech tagging, dependency parsing, contextual and synonymy vector generation with the FiBER transformer model. An extensive unbiased crowd-sourced evaluation of the proposed framework has been performed, showing an acceptability rate (total and partial combined) of 95%. Time and space analyses of our framework also demonstrate the scalability of the proposed solution.

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.

Abstract In autonomous and robotic systems, the functional requirements (FRs) and non‐functional requirements (NFRs) are gathered from multiple stakeholders. The different stakeholder requirements are associated with different components of the robotic system and with the contexts in which the system may operate. This aggregation of requirements from different sources (multiple stakeholders) often results in inconsistent or conflicting sets of requirements. Conflicts among NFRs for robotic systems heavily depend on features of actual execution contexts. It is essential to analyze the inconsistencies and conflicts among the requirements in the early planning phase to design the robotic systems in a systematic manner. In this work, we design and experimentally evaluate a framework, called SCARS, providing: (a) a domain‐specific language extending the ROS2 Domain Specific Language (DSL) concepts by considering the different environmental contexts in which the system has to operate, (b) support to analyze their impact on NFRs, and (c) the computation of the optimal degree of NFR satisfaction that can be achieved within different system configurations. The effectiveness of SCARS has been validated on the iRobot Create3 robot using Gazebo simulation.

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.

Named entity recognition (NER) is a natural language processing task that has been used in Requirements Engineering for the identification of entities such as actors, actions, operators, resources, events, GUI elements, hardware, APIs, and others. NER might be particularly useful for extracting key information from Software Requirements Specification documents, which provide a blueprint for software development. However, a common challenge in this domain is the lack of annotated data. In this article, we propose and analyze two zero-shot approaches for NER in the requirements engineering domain. These are found to be particularly effective in situations where labeled data is scarce or non-existent. The first approach is a template-based zero-shot learning mechanism that uses the prompt engineering approach and achieves 93% accuracy according to our experimental results. The second solution takes an orthogonal approach by transforming the entity recognition problem into a question-answering task which results in 98% accuracy. Both zero-shot NER approaches introduced in this work perform better than the existing state-of-the-art solutions in the requirements engineering domain.

Abstract In the design of autonomous systems, it is important to consider the preferences of the interested parties to improve the user experience. These preferences are often associated with the contexts in which each system is likely to operate. The operational behavior of a system must also meet various non-functional requirements (NFRs), which can present different levels of conflict depending on the operational context. This work aims to model correlations between the individual contexts and the consequent conflicts between NFRs. The proposed approach is based on analyzing the system event logs, tracing them back to the leaf elements at the specification level and providing a contextual explanation of the system’s behavior. The traced contexts and NFR conflicts are then mined to produce Context-Context and Context-NFR conflict sequential rules. The proposed Contextual Explainability (ConE) framework uses BERT-based pre-trained language models and sequential rule mining libraries for deriving the above correlations. Extensive evaluations are performed to compare the existing state-of-the-art approaches. The best-fit solutions are chosen to integrate within the ConE framework. Based on experiments, an accuracy of 80%, a precision of 90%, a recall of 97%, and an F1-score of 88% are recorded for the ConE framework on the sequential rules that were mined.

An emerging feature of mobile application software is the need to quickly produce new versions to solve problems that emerged in previous versions. This helps adapt to changing user needs and preferences. In a continuous software development process, the user reviews collected by the apps themselves can play a crucial role to detect which components need to be reworked. This paper proposes a novel framework that enables software companies to drive their technology value stream based on the feedback (or reviews) provided by the end-users of an application. The proposed end-to-end framework exploits different Natural Language Processing (NLP) tasks to best understand the needs and goals of the end users. We also provide a thorough and in-depth analysis of the framework, the performance of each of the modules, and the overall contribution in driving the technology value stream. An analysis of reviews with sixteen popular Android Play Store applications from various genres over a long period of time provides encouraging evidence of the effectiveness of the proposed approach.

Requirement prioritization is an inherently important step in the DevOps framework. Unfortunately, the prioritization process often disregards the non-functional requirements and the possible conflicts among them. This implies that unresolved dependencies and conflicts would be identified at integration time only, which may lead to major refactoring issues. We introduce CARO a new tool that generates an ordering among the requirements based on conflicts and dependencies among the requirements. The tool provides a quantitative risk evaluation framework along with risk mitigation strategies based on conflicts and dependencies among the requirements.

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).

Dependency information (data- and/or control-dependencies) among program variables and program statements is playing crucial roles in a wide range of software-engineering activities, e.g., program slicing, information flow security analysis, debugging, code-optimization, code-reuse, code-understanding. Most existing dependency analyzers focus on mainstream languages and they do not support database applications embedding queries and data-manipulation commands. The first extension to the languages for relational database management systems, proposed by Willmor et al. in 2004, suffers from the lack of precision in the analysis primarily due to its syntax-based computation and flow insensitivity. Since then no significant contribution is found in this research direction. This paper extends the Abstract Interpretation framework for static dependency analysis of database applications, providing a semantics-based computation tunable with respect to precision. More specifically, we instantiate dependency computation by using various relational and non-relational abstract domains, yielding to a detailed comparative analysis with respect to precision and efficiency. Finally, we present a prototype$\sf{ semDDA}$, asemantics-basedDatabaseDependencyAnalyzer integrated with various abstract domains, and we present experimental evaluation results to establish the effectiveness of our approach. We show an improvement of the precision on an average of 6 percent in the interval, 11 percent in the octagon, 21 percent in the polyhedra and 7 percent in the powerset of intervals abstract domains, as compared to their syntax-based counterpart, for the chosen set of Java Server Page (JSP)-based open-source database-driven web applications as part of the GotoCode project.

Leveraging the benefits of service computing technologies for Internet of Things (IoT) can help in rapid system development, composition and deployment. But due to the massive scale, computational and communication constraints, existing software service models cannot be directly applied for IoT based systems. Service discovery and composition mechanism need to be decentralized unlike majority of other service models. Moreover, IoT services' interfaces require to be light weight and able to expose the device profile for seamless discovery onto the IoT based system infrastructure. In addition to this, the "things" data should be associated with its present context. To address these issues, this paper proposes a formal model for IoT services. The service model includes the physical property of "things" and exposes it to the user. It also associates the context with the "things" output, which in turn helps in extracting relevant information from the "things" data. To evaluate our IoT service model, a weather monitoring system and its associated services are implemented using node.js [31]. The service data is mapped to SSN ontology for generating context-rich RDF data. This way, the proposed IoT service model can expose the device profile to the user and incorporate relevant context information with the things data.

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.

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.

Security of robotics systems, as well as of the related middleware infrastructures, is a critical issue for industrial and domestic IoT, and it needs to be continuously assessed throughout the whole development lifecycle. The next generation open source robotic software stack, ROS2, is now targeting support for Secure DDS, providing the community with valuable tools for secure real world robotic deployments. In this work, we introduce a framework for procedural provisioning access control policies for robotic software, as well as for verifying the compliance of generated transport artifacts and decision point implementations.

We present a refined segmentation abstract domain for the analysis of strings in the C programming language, properly extending the parametric segmentation approach to array representation introduced by P. Cousot et al. to the case of text values. In particular, we capture the so-called string of interest of an array of char, in order to distinguish well-formed string arrays. A concrete and abstract semantics of the main C header file string.h functions are worked out in full detail.

Domain-Specific Languages (DSL's) offer language-level abstractions that General-Purpose Languages do not offer, thus speeding up the implementation of the solution of problems within a specific domain. Developers have the choice of developing a DSL by building an interpreter/compiler for it, which is a hard and time-consuming task, or embedding it in a host language, thus speeding up the development process but losing several advantages that having a dedicated compiler might bring. In this work we present a meta-compiler called Metacasanova, whose meta-language is based on operational semantics. Then, we propose a language extension with functors and modules that allows to embed the type system of a language definition inside the meta-type system of Metacasanova and improves the performance of manipulating data structures at run-time. Our results show that Metacasanova dramatically reduces the code lines required to develop a compiler, and that the running time of the Meta-program is improved by embedding the host language type system in the meta-type system with the use of functors in the meta-language.

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.

Smart Grid is an integrated power grid with a. reliable, communication network running in parallel towards providing two way communications in the grid.It's trivial to mention that a network like this would connect a huge number of IP-enabled devices.IPv6 that offers 18-bit address space becomes an obvious choice in this context.In a smart grid, functionalities like neighborhood discovery, autonomic address configuration of a node or its router identification may often be invoked whenever newer equipments are introduced for capacity enhancement at some level of hierarchy.In IPv6, these basic functionalities like neighborhood discovery, autonomic address configuration of networking require to use Internet Control Message Protocol version 6 (ICMPv6).Such usage may lead to security breaches in the grid as a result of possible abuses of ICMPv6 protocol.In this paper, some potential newer attacks on Smart Grid have been discussed.Subsequently, intrusion prevention mechanisms for these attacks are proposed to plugin the threats.

We introduce Tukra, a tool that allows the practical evaluation of abstract program slicing algorithms. The tool exploits the notions of statement relevancy, semantic data dependences and conditional dependences. The combination of these three notions allows Tukra to refine traditional syntax-based program dependence graphs, generating more accurate slices. We provide the architecture of the tool, some snapshots describing how it works, and some preliminary experimental results giving evidence of the accuracy improvements it supports.

In this paper, we propose an obfuscation/ deobfuscation based technique to detect the presence of possible SQL Injection Attacks (SQLIA) in a query before submitting it to a DBMS. This technique combines static and dynamic analysis. In the static phase, the queries in the application are replaced by queries in obfuscated form. The main idea behind obfuscation is to isolate all the atomic formulas from other control elements of the query. During the dynamic phase, the user inputs are merged into the obfuscated atomic formulas, and the dynamic verifier analysis the presence of possible SQLIA at atomic formula level. Finally, a deobfuscation step is performed to recover the original query before submitting it to the DBMS.

Interpretation, one of the most applied techniques for semantics based static analysis of software, is based on two main key-concepts: the correspondence between concrete and abstract semantics through Galois connections/insertions, and the feasibility of a fixed point computation of the abstract semantics, through the fast convergence of widening operators. The latter point is crucial to ensure the scalability of the analysis to large software systems. In this paper, we investigate which properties are necessary to support a systematic design of widening operators, by discussing and comparing different definitions in the literature, and by proposing various ways to combine them. In particular, we prove that, for Galois insertions, widening is preserved by abstraction, and we show how widening operators can be combined for the cartesian and reduced product of abstract domains.

This paper presents a novel technique for analyzing security protocols based on an abstraction of the program semantics. This technique is based on a novel structure called causal graph which captures the causality among program events within a finite graph. A core property of causal graphs is that they abstract away from the multiplicity of protocol sessions, hence constituting a concise tool for reasoning about an even infinite number of concurrent protocol sessions; deciding security only requires a traversal of the causal graph, thus yielding a decidable, and typically very efficient, approach for security protocol analysis. Additionally, causal graphs allow for dealing with different security properties such as secrecy and authenticity in a uniform manner. Both the construction of the causal graph from a given protocol description and the analysis have been fully automated and tested on several example protocols from the literature.

Reduced product of abstract domains is a rather well-known operation for domain composition in abstract interpretation. In this article, we study its inverse operation, introducing a notion of domain complementation in abstract interpretation. Complementation provides as systematic way to design new abstract domains, and it allows to systematically decompose domains. Also, such an operation allows to simplify domain verification problems, and it yields space-saving representations for complex domains. We show that the complement exists in most coses, and we apply complementation to three well-know abstract domains, notably to Cousot and Cousot's interval domain for integer variable analysis, to Cousot and Cousot's domain for comportment analysis of functional languages, and to the domain Sharing for aliasing analysis of logic languages.

Type analysis of Prolog is of primary importance for high-performance compilers, since type information may lead to better indexing and to sophisticated specializations of unification and built-in predicates to name a few. However, these optimizations often require a sophisticated type inference system capable of inferring disjunctive and recursive types and hence expensive in computation time.

Abstract interpretation [7] is a systematic methodology to design static program analysis which has been studied extensively in the logic programming community, because of the potential for optimizations in logic programming compilers and the sophistication of the analyses which require conceptual support. With the emergence of efficient generic abstract interpretation algorithms for logic programming, the main burden in building an analysis is the abstract domain which gives a safe approximation of the concrete domain of computation. However, accurate abstract domains for logic programming are often complex because of the variety of analyses to perform their interdependence, and the need to maintain structural information. The purpose of this paper is to propose conceptual and software support for the design of abstract domains. It contains two main contributions: the notion of open product and a generic pattern domain. The open product is a new way of combining abstract domains allowing each combined domain to benefit from information from the other components through the notions of queries and open operations. The open product is general-purpose and can be used for other programming paradigms as well. The generic pattern domain Pat (R)automatically upgrades a domain D with structural information yielding a more accurate domain Pat (D) without additional design or implementation cost. The two contributions are orthogonal and can be combined in various ways to obtain sophisticated domains while imposing minimal requirements on the designer. Both contributions are characterized theoretically and experimentally and were used to design very complex abstract domains such as PAT(OProp⊗OMode⊗OPS) which would be very difficult to design otherwise. On this last domain, designers need only contribute about 20% (about 3,400 lines) of the complete system (about 17,700 lines).

The abstract domain Prop for analyzing variable groundness in logic programs is considered. This domain consists of (equivalence classes of) propositional formulas whose propositional variables correspond to program variables with truth assignments indicating which program variables are ground. Some ambiguity remains about precisely which formula should be included in Prop so that all interesting sets of program execution states (substitutions) have a unique representation. This ambiguity is clarified by characterizing, both semantically and syntactically, the appropriate definition of Prop. The use of propositional formulas for representing properties of substitutions of a different type than groundness, such as freeness and independence of variables, is discussed.>

article Abstract interpretation of logic programs: an abstract domain for groundness, sharing, freeness and compoundness analysis Share on Authors: Agostino Cortesi Dept. of Mathematics, University of Padova, Via Belzoni 7, I-35131 Padova, Italy Dept. of Mathematics, University of Padova, Via Belzoni 7, I-35131 Padova, ItalyView Profile , Gilbert Filé Dept. of Mathematics, University of Padova, Via Belzoni 7, I-35131 Padova, Italy Dept. of Mathematics, University of Padova, Via Belzoni 7, I-35131 Padova, ItalyView Profile Authors Info & Claims ACM SIGPLAN NoticesVolume 26Issue 9Sept. 1991 pp 52–61https://doi.org/10.1145/115866.115872Published:01 May 1991 23citation291DownloadsMetricsTotal Citations23Total Downloads291Last 12 Months4Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access