1,720,980 research outputs found
A generic framework for multilanguage analysis
No full textL'analisi statica di programmi scritti in più linguaggi di programmazione è impegnativa. Gli analizzatori tradizionali analizzano un singolo linguaggio, o un gruppo di linguaggi simili, per adattare l'analisi alle sue (o loro) caratteristiche. Analisi dell'intera applicazione possono quindi essere eseguite solo da una combinazione di analizzatori. Poiché sono necessarie più analisi, questo non consente all'analisi statica di avere un impatto significativo negli scenari del mondo reale.
Questa tesi descrive LiSA, un framework generico in cui è possibile definire analisi statiche multilinguaggio attraverso l'interpretazione astratta. LiSA è una libreria Java open source che fornisce l'infrastruttura completa necessaria per lo sviluppo di analizzatori statici. LiSA è stata istanziata per due casi d'uso reali. GoLiSA (un analizzatore per Go basato su LiSA) applica analisi di information flow per individuare costrutti non deterministici che influenzano lo stato della blockchain. Invece, PyLiSA (un analizzatore per Python basato su LiSA) fornisce un'astrazione per il software che si occupa di dataframe. Un terzo POC dimostra la capacità di LiSA di analizzare più linguaggi in un'unica analisi attraverso, scoprendo una vulnerabilità IoT che su codice C++ e Java.
Inoltre, questa tesi definisce SARL, un linguaggio che può essere utilizzato per modellare come framework e librerie interagiscono con l'applicazione analizzata, e TARSIS, un'astrazione di stringhe come linguaggi regolari
MichelsonLiSA: A Static Analyzer for Tezos
No full textSmart contracts are immutable code deployed in a blockchain, whose execution modifies its global state. Code im-mutability leads to immutable bugs. To prevent such bugs, static program analysis infers information about the behavior of the code, statically, before code execution and deployment. This paper introduces MichelsonLiSA, a static analyzer based on abstract interpretation for the verification of smart contracts written in the Michelson low-level language of the Tezos blockchain. It applies MichelsonLiSA to the identification of security issues arising from cross-contract invocations
Challenges of software verification
Full text linkSoftware 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. This special issue of Software Tools for Technology Transfer presents novel theoretical directions and practical applications of these techniques. The papers in this special issue are extended versions of selected symposium papers from the proceedings of the 3rd Challenges of Software Verification Symposium (CSV), which took place at the Ca’ Foscari University of Venice, Venice, Italy, June 6–7, 2024
Stability: An Abstract Domain for the Trend of Variation of Numerical Variables
Full text linkState-of-the-art abstract domains for static analysis typically focus on over-approximating either the values a variable can hold at a specific program point or the relational dependencies among variables. In this paper, we aim to capture the trend of numerical values during program executions (e.g., increasing, decreasing, or stable) relative to preceding states. By integrating the Stability domain with numerical domains, we can verify co-/contra-variance relationships among potentially unrelated variables. This approach has promising applications for anomaly detection in complex software systems, and for the verification of functional requirements
Inference of access policies through static analysis
Full text linkRobot 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
Teaching Through Practice: Advanced Static Analysis with LiSA
Full text linkNowadays, ready-to-use libraries and code generation are often used to streamline and speed up the software development process. The resulting programs are thus a collection of different modules that cooperate: proving their safety and reliability is increasingly complex, requiring sound formal techniques, such as static program analysis. However, while teaching static analysis to master’s or PhD students, the predominant focus on theoretical concepts often leaves limited space for students to engage with the practical aspects of implementing static analyses and is limited to developing elementary ones. In this paper, we show how the infrastructure offered by LiSA can be exploited to learn how to implement advanced static analyses, such as string and relational numerical analyses, just focusing on their distinctive aspects. This would help to narrow the gap between theoretical and practical contents in static analysis courses, bringing the learning experience beyond the rudimentary implementation of static analyses to more sophisticated applications
LiSA: A Generic Framework for Multilanguage Static Analysis
No full textModern software engineering revolves around distributed applications. From IoT networks to client-server infrastructures, the application code is increasingly being divided into separate sub programs interacting with each other. As they are completely independent from each other, each such program is likely to be developed in a separate programming language, choosing the best fit for the task to at hand. From a static program analysis perspective, taking on a mixture of languages is challenging. This paper defines a generic framework where modular multilanguage static analyses can be defined through the abstract interpretation theory. The framework has been implemented in LiSA (Library for Static Analysis), an open-source Java library that provides the complete infrastructure necessary for developing static analyzers. LiSA strives to be modular, ensuring that all components taking part in the analysis are both easy to develop and highly interchangeable. LiSA also ensures that components are parametric to all language specific features: semantics, execution model and memory model are not directly encoded within the components themselves. A proof-of-concept instantiation is provided, demonstrating LiSA’s capability to analyze multiple languages in a single analysis through the discovery of an IoT vulnerability spanning C++ and Java code
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
