Reproducibility is the ability of recreating identical binaries under pre-defined build environments. Due to the need of quality assurance and the benefit of better detecting attacks against build environments, the practice of reproducible builds has gained popularity in many open-source software repositories such as Debian and Bitcoin. However, identifying the unreproducible issues remains a labour intensive and time consuming challenge, because of the lacking of information to guide the search and the diversity of the causes that may lead to the unreproducible binaries. In this paper we propose an automated framework called RepLoc to localize the problematic files for unreproducible builds. RepLoc features a query augmentation component that utilizes the information extracted from the build logs, and a heuristic rule-based filtering component that narrows the search scope. By integrating the two components with a weighted file ranking module, RepLoc is able to automatically produce a ranked list of files that are helpful in locating the problematic files for the unreproducible builds. We have implemented a prototype and conducted extensive experiments over 671 real-world unreproducible Debian packages in four different categories. By considering the topmost ranked file only, RepLoc achieves an accuracy rate of 47.09%. If we expand our examination to the top ten ranked files in the list produced by RepLoc, the accuracy rate becomes 79.28%. Considering that there are hundreds of source code, scripts, Makefiles, etc., in a package, RepLoc significantly reduces the scope of localizing problematic files. Moreover, with the help of RepLoc, we successfully identified and fixed six new unreproducible packages from Debian and Guix.
It is undeniable that artificial intelligence (AI) and blockchain concepts are spreading at a phenomenal rate. Both technologies have distinct degree of technological complexity and multi-dimensional business implications. However, a common misunderstanding about blockchain concept, in particular, is that blockchain is decentralized and is not controlled by anyone. But the underlying development of a blockchain system is still attributed to a cluster of core developers. Take smart contract as an example, it is essentially a collection of codes (or functions) and data (or states) that are programmed and deployed on a blockchain (say, Ethereum) by different human programmers. It is thus, unfortunately, less likely to be free of loopholes and flaws. In this article, through a brief overview about how artificial intelligence could be used to deliver bug-free smart contract so as to achieve the goal of blockchain 2.0, we to emphasize that the blockchain implementation can be assisted or enhanced via various AI techniques. The alliance of AI and blockchain is expected to create numerous possibilities.
L'interpretazione astratta è una teoria che formalizza l'approssimazione conservativa della semantica di sistemi informatici hardware e software, focalizzandosi su alcune proprietà, che espresse mediante opportune strutture algebriche (domini astratti) possono essere calcolate in modo corretto (anche se non completo). Una grande varietà di domini astratti può essere elaborata, a aseconda dei contesti di applicazione, e con scelta dei domini astratti è possibile modulare in modi diversi precisione e complessità computazionale. Questa tesi considera l'applicazione di tecniche di Interpretazione Astratta in tre diversi scenari: Program slicing; Watermarking di database relazionali; Watermarking del codice sorgente di programmi. Relativamente al Program slicing, viene proposto un raffinamento delle tecniche tradizionali già presenti in letteratura. Molto spesso, siamo interessati a una specifica proprietà delle variabili in un criterio di slicing, piuttosto che ai suoi effettivi valori. Questo è il caso, ad esempio, quando si analizza la non-interferenza in language-based security, dove le astrazioni entrano in gioco per modellare il potere osservativo degli attaccanti. In questo scenario, lo slicing tiene in considerazione le proprietà astratte delle variabili e le dipendenze astratte. Questo approccio allo slicing, non è solo la generalizzazione della tecnica tradizionale, ma offre nuovi spunti nelle relazioni tra diverse aree di ricerca dell'informatica. Un secondo scenario di applicazione delle tecniche di Interpretazione Astratta è la progettazione di watermarking di database relazionali, la cui rilevanza è legata al fatto che in Internet è molto importante preservare i diritti di proprietà nei database relazionali mantenuti in outsourcing. In tale ambito, viene proposta una tecnica di watermarking senza distorsione, che migliora la verifica dell'integrità dei database relazionali utilizzando un meccanismo di autenticazione pubblica. L'ultimo scenario considerato è quello del Watermarking del codice sorgente di programmi: all'aumentare della quantità di codice sorgente distribuito sul web, la protezione e il rilevamento delle proprietà del software è diventata una questione importante. Nella tesi, viene presentato uno schema di watermarking software a chiave pubblica (watermarking asimmetrico), basato su tecniche di trasformazione che preservano la semantica, e che è simile nello spirito alle zero-knowledge proofs. L'approccio proposto si pone come un'alternativa alla cifratura e l'autenticazione software piuttosto che come uno strumento per la protezione del copyright.
Modern computing platforms strive to support mobile code without putting system security at stake. These platforms can be viewed as open systems, as the mobile code adds new components to the running system. Establishing that such platforms function correctly can be divided into two steps. First, it is shown that the system functions correctly regardless of the mobile components that join it, provided that they satisfy certain assumptions. These assumptions can, for instance, restrict the behavior of the component to ensure that the security policy of the platform is not violated. Second, the mobile component is checked to satisfy its assumptions, before it is allowed to join the system. This thesis presents algorithmic verification techniques to support this methodology. In the first two parts, we present techniques for the verification of open systems relative to the given component assumptions. In the third part, a technique for the quick certification of mobile code is presented for the case where a particular type of program rewriting is used as a means of enforcing the component assumptions.In the first part of this study, we present a framework for the verification of open systems based on explicit state space representation. We propose Extended Modal Transition Systems (EMTS) as a suitable structure for representing the state space of open systems when assumptions on components are written in the modal μ-calculus. EMTSs are based on the Modal Transition Systems (MTS) of Larsen and provide a formalism for graphical specification and facilitate a thorough understanding of the system by visualization. In interactive verification, this state space representation enables proof reuse and aids the user guiding the verification process. We present a construction of state space representations from process algebraic open system descriptions based on a maximal model construction for the modal μ-calculus. The construction is sound and complete for systems with a single unknown component and sound for those without dynamic process reation. We also suggest a tableau-based proof system for establishing temporal properties of open systems represented as EMTS. The proof system is sound in general and complete for prime formulae.The problem of open system correctness also arises in compositional verification, where the problem of showing a global property of a system is reduced to showing local properties of components. In the second part, we extend an existing compositional verification framework for Java bytecode programs. The framework employs control flow graphs with procedures to model component implementations and open systems for the purpose of checking control-flow properties. We generalize these models to capture exceptional and multi-threaded behavior. The resulting control flow graphs are specifically tailored to support the compositional verification principle; however, they are sufficiently intuitive and standard to be useful on their own. We describe how the models can be extracted from program code and give preliminary experimental results for our implementation of the extraction of control flow graphs with exceptions. We also discuss further tool support and practical applications of the method.In the third part of the thesis, we develop a technique for the certification of safe mobile code, by adapting the proof-carrying code scheme of Necula to the case of security policies expressed as security automata. In particular, we describe how proofs of policy compliance can be automatically generated for programs that include a monitor for the desired policy. A monitor is an entity that observes the execution of a program and terminates the program if a violation to the property is about to occur. One way to implement such a monitor is by rewriting the program to make it self-monitoring. Given a property, we characterize self-monitoring of Java bytecode programs for this property by an annotation scheme with annotations in the style of Floyd-Hoare logics. The annotations generated by this scheme can be extended in a straightforward way to form a correctness proof in the sense of axiomatic semantics of programs. The proof generated in this manner essentially establishes that the program satisfies the property because it contains a monitor for it. The annotations that comprise the proofs are simple and efficiently checkable, thus facilitate certification of mobile code on devices with restricted computing power such as mobile phones.