No description available.

<p dir="ltr">Deep Neural Networks (DNNs) have been deployed on edge devices for numerous applications, ranging from computer vision, speech recognition, and anomaly detection. When deployed on edge devices, dedicated DNN compilers are used to compile DNNs into binaries to exploit instruction set architectures’ (ISAs’) features and hardware accelerators (e.g., NPU, GPU). These DNN binaries on edge devices process sensitive user information, conduct critical missions, and are considered confidential intellectual property.</p><p dir="ltr">From the security standpoint, the ability to reverse engineer such binaries (i.e., recovering the original, high-level representation of the implemented DNN) enables several applications, such as DNN models stealing, gray/white-box adversarial machine learning attacks and defenses, and backdoor detection. However, no existing reverse engineering technique can recover a high-level representation of a DNN model from its compiled binary code.</p><p dir="ltr">In this dissertation, we propose the following pioneering research for reverse engineering DNN on the edge device. (i) We design and implement the first compiler- and ISA-agnostic DNN decompiler, DnD, with the static analysis technique, capable of extracting DNN models from DNN binaries running on CPU-only devices without the hardware accelerator. We show that our decompiler can perfectly recover DNN models from different DNN binaries. Furthermore, it can extract DNN models used by real-world micro-controllers and enable white-box adversarial machine learning attacks against the DNN models. (ii) We design and implement a novel data-driven approach, NeuroScope, based on dynamic analysis and machine learning to reverse engineer DNN binaries. This compiler-independent and code-feature-free approach supports a larger variety of DNN binaries across different DNN compilers and hardware platforms. We demonstrate its capability by using it to reverse engineer DNN binaries unsupported by previous approaches with high accuracy. Moreover, we showcase how NeuroScope can be used to reverse engineer a proprietary DNN binary compiled with a closed-source compiler and enable gray-box adversarial machine learning attacks.</p>

Formal verification of software systems has historically focused on verifying properties at the source code (abstract language) level (e.g., C++, Java, Python), as the language semantics are more amenable to use by mathematical libraries. However, this approach comes with limitations. Firstly, not all software has source code. Secondly, the source code may be unavailable for licensing reasons. Thirdly, even if the source code is available, formal verification at the source code level generally assumes that the compiler is trustworthy and mathematically sound. This dissertation addresses challenges with lifting the abstraction of software binaries to support formal verification and reasoning toward bridging the semantic gap. The semantic gap is the loss and obfuscation of program meaning that occurs as a result of compiling source code into software binaries. This work's primary application is verifying safety-critical systems where source code is unavailable. The x86-64 Instruction Set Architecture (ISA) was chosen due to its applicability to a wide range of relevant deployed software. As a necessary dependency for the formal verification of software binaries, a machine model of the ISA is required. The machine model is analogous to the language semantics necessary when reasoning over source code. The x86-64 ISA was also chosen because, in addition to being complex, it lacked a formal specification, making it a more challenging target. Historically, much research in the area of reasoning over x86 software binaries has focused on small fragments of code, utilizing a small subset of the ISA that could be handwritten formally, limiting research to a small subset of real-world software. The first contribution of this dissertation addresses these limitations, presenting a robust hardware-derived formal executable machine model of the x86-64 ISA, supporting 1,625 instruction variants expressed as small-step operational semantics embedded within an Interactive Theorem Prover (ITP) (a 4-fold increase over prior work). The second contribution of this dissertation presents a largely automated methodology for generating formally proven equivalence theorems between decompiled x86-64 machine code and big-step operational semantics. These formally proven abstract representations of software binaries allow one to construct correctness proofs per block. To support this, we developed improved Decompilation-into-logic and formal symbolic execution techniques. We then applied this methodology to several case studies, including examples heavily relying on floating-point instructions and real-world examples. This dissertation's third contribution presents efforts to bridge the semantic gap further and tie the results to formal verification techniques commonly utilized over source code. It presents a first-of-the-art approach to leveraging a hardware-derived model derived from machine learning in software binary formal verification efforts. It introduces a library of 628 proven simplification lemmas designed to lift the abstraction of big-step operational semantics to a form more useful to proof engineers. A methodology for performing axiomatic reasoning across blocks is presented, with case studies demonstrating, for software binaries, standard formal verification techniques typically applicable to source code. Lastly, this dissertation explores a methodology for sound software binary diversity to employ a moving target defense strategy with associated security benefits. Toward bridging the semantic gap between software binaries and source code, this work demonstrates large-scale black-box software binary formal verification in settings where source code is unavailable, on a hardware-derived machine model, as well as a sound software binary diversity approach for moving target defense. / Doctor of Philosophy / Between the optimization and obfuscation of compilers and a lack of comprehensive small-step operational semantics, lifting x86-64 software binaries and formally verifying them to a specification has been difficult. As a result, most formal verification methodologies operate on source code instead of software binaries. Operating systems and other safety-critical software, however, often leverage custom assembly code or a hybrid of C++ and assembly for performance considerations, which would not work with standard formal verification methodologies that operate on source code. This dissertation demonstrates methods for lifting the abstraction of software binaries, leveraging a hardware-derived machine model toward bridging the semantic gap to enable more traditional formal verification methodologies to work, as well as a sound software binary diversity approach for moving target defense.

Thesis (MSc)--Stellenbosch University, 2013. / ENGLISH ABSTRACT: In this dissertation we present a software tool, Artemis, that symbolically executes Java virtual machine bytecode to find bugs and automatically generate test cases to trigger the bugs found. Symbolic execution is a technique of static software analysis that entails analysing code over symbolic inputs—essentially, classes of inputs—where each class is formulated as constraints over some input domain. The analysis then proceeds in a path-sensitive way adding the constraints resulting from a symbolic choice at a program branch to a path condition, and branching non-deterministically over the path condition. When a possible error state is reached, the path condition can be solved, and if soluble, value assignments retrieved to be used to generate explicit test cases in a unit testing framework. This last step enhances confidence that bugs are real, because testing is forced through normal language semantics, which could prevent certain states from being reached. We illustrate and evaluate Artemis on a number of examples with known errors, as well as on a large, complex code base. A preliminary version of this work was successfully presented at the SAICSIT conference held on 1–3 October 2012, in Centurion, South Africa. / AFRIKAANSE OPSOMMING: In die dissertasie bied ons ’n stuk sagtewaregereedskap, Artemis, aan wat biskode van die Java virtuele masjien simbolies uitvoer om foute op te spoor en toetsgevalle outomaties voort te bring om die foute te ontketen. Simboliese uitvoering is ’n tegniek van statiese sagteware-analise wat behels dat kode oor simboliese toevoere—in wese, klasse van toevoer—geanaliseer word, waar elke klas geformuleer word as beperkinge oor ’n domein. Die analise volg dan ’n pad-sensitiewe benadering deur die domeinbeperkinge, wat volg uit ’n simboliese keuse by ’n programvertakking, tot ’n padvoorwaarde by te voeg en dan nie-deterministies vertakkings oor die padvoorwaarde te volg. Wanneer ’n moontlike fouttoestand bereik word, kan die padvoorwaarde opgelos word, en indien dit oplaasbaar is, kan waardetoekennings verkry word om eksplisiete toetsgevalle in ’n eenheidstoetsingsraamwerk te formuleer. Die laaste stap verhoog vertroue dat die foute gevind werklik is, want toetsing word deur die normale semantiek van die taal geforseer, wat sekere toestande onbereikbaar maak. Ons illustreer en evalueer Artemis met ’n aantal voorbeelde waar die foute bekend is, asook op ’n groot, komplekse versameling kode. ’n Voorlopige weergawe van die´ werk is suksesvol by die SAICSIT-konferensie, wat van 1 tot 3 Oktober 2012 in Centurion, Suid-Afrika, gehou is, aangebied.

<div>In a potentially hostile networked environment, a large diversity of security mechanisms with varying degree of sophistication are being deployed to protect valuable computer systems and digital assets. </div><div><br></div><div>While many competing implementations of similar security mechanisms are available in the current software development landscape, the robustness and reliability of such implementations are often overlooked, resulting in exploitable flaws in system deployments. In this dissertation, we systematically evaluate implementations of security mechanisms that are deployed in the wild. First, we examine how content distribution applications on the Android platform control access to their multimedia contents. With respect to a well-defined hierarchy of adversarial capabilities and attack surfaces, we find that many content distribution applications, including that of some world-renowned publications and streaming services, are vulnerable to content extraction due to the use of unjustified assumptions in their security mechanism designs and implementations. Second, we investigate the validation logic of X.509 certificate chains as implemented in various open-source TLS libraries. X.509 certificates are widely used in TLS as a means to achieve authentication. A validation logic that is overly restrictive could lead to the loss of legitimate services, while an overly permissive implementation could open door to impersonation attacks. Instead of manual analysis and unguided fuzzing, we propose a principled approach that leverages symbolic execution to achieve better coverage and uncover logical flaws that are buried deep in the code. We find that many TLS libraries deviate from the specification. Finally, we study the verification of RSA signatures, as specified in the PKCS#1 v1.5 standard, which is widely used in many security-critical network protocols. We propose an approach to automatically generate meaningful concolic test cases for this particular problem, and design and implement a provenance tracking mechanism to assist root-cause analysis in general. Our investigation revealed that several crypto and IPSec implementations are susceptible to new variants of the Bleichenbacher low-exponent signature forgery.</div>

En raison de la complexité croissante des systèmes réactifs, le test est devenu un des éléments essentiels dans le processus de leur développement. Les tests de conformité avec des méthodes formelles concernent la correction du contrôle fonctionnel, par le biais des tests d'un système en boîte noire avec une spécification formelle du système. Les techniques passives de test sont utilisées lorsque l’exécution des systèmes testés ne peut pas être perturbée ou l'interface du système n'est pas fournie. Les techniques passives de test sont fondées sur l'observation et la vérification des propriétés du comportement d'un système sans interférer avec son fonctionnement normal. Les tests contribuent également à établir les comportements anormaux pendant l’exécution sur la base de l'observation de toute déviation d'un comportement prédéterminé. L'objectif principal de cette thèse est de présenter une nouvelle approche pour la mise en place des tests passifs fondés sur l'analyse des parties contrôle et données du système sous test. Au cours des dernières décennies, de nombreuses théories et outils ont été développés pour effectuer les tests de conformité. De fait, les spécifications ou les propriétés des systèmes réactifs sont souvent modélisés par différentes variantes de Labeled Transition Systems (LTS). Toutefois, ces méthodes ne prennent pas explicitement en compte les parties données du système, étant donné que le modèle sous-jacent de LTS n’est pas en mesure de le faire. Par conséquent, avec ces approches il est nécessaire d'énumérer les valeurs des données avant la modélisation du système. Cela conduit souvent au problème de l'explosion combinatoire de l'état-espace. Pour palier à cette limitation, nous avons étudié un modèle appelé Input-Output Symbolic Transition Systems (IOSTS) qui inclut explicitement toutes les données d'un système réactif. De nombreuses techniques de tests passives prennent uniquement en considération la partie du contrôle du système en négligeant les données, ou elles sont confrontées à une quantité énorme de données du processus. Dans notre approche, nous prenons en compte la partie contrôle et données en intégrant les concepts d'exécution symbolique et nous améliorons l'analyse de traces en introduisant des techniques de slicing des traces d’exécution. Les propriétés sont décrites à l'aide d'IOSTS et nous illustrons dans notre approche comment elles peuvent être testées sur l'exécution réelle des traces en optimisant l'analyse. Ces propriétés peuvent être conçues pour tester la conformité fonctionnelle d'un protocole ainsi que des propriétés de sécurité. Au-delà de l'approche théorique, nous avons développé un outil logiciel qui implémente les algorithmes présentés dans nos travaux. Enfin, comme preuve de concept de notre approche et de l'outil logiciel, nous avons appliqué les techniques à deux études de cas réels : le protocole SIP et le protocole Bluetooth / Due to the increasing complexity of reactive systems, testing has become an important part in the process of the development of such systems. Conformance testing with formal methods refers to checking functional correctness, by means of testing, of a black-box system under test with respect to a formal system specification, i.e., a specification given in a language with a formal semantics. In this aspect, passive testing techniques are used when the implementation under test cannot be disturbed or the system interface is not provided. Passive testing techniques are based on the observation and verification of properties on the behavior of a system without interfering with its normal operation, it also helps to observe abnormal behavior in the implementation under test on the basis of observing any deviation from the predefined behavior. The main objective of this thesis is to present a new approach to perform passive testing based on the analysis of the control and data part of the system under test. During the last decades, many theories and tools have been developed to perform conformance testing. However, in these theories, the specifications or properties of reactive systems are often modeled by different variants of Labeled Transition Systems (LTS). However, these methodologies do not explicitly take into account the system's data, since the underlying model of LTS are not able to do that. Hence, it is mandatory to enumerate the values of the data before modeling the system. This often results in the state-space explosion problem. To overcome this limitation, we have studied a model called Input-Output Symbolic Transition Systems (IOSTS) which explicitly includes all the data of a reactive system. Many passive testing techniques consider only the control part of the system and neglect data, or are confronted with an overwhelming amount of data values to process. In our approach, we consider control and data parts by integrating the concepts of symbolic execution and we improve trace analysis by introducing trace slicing techniques. Properties are described using Input Output Symbolic Transition Systems (IOSTSs) and we illustrate in our approach how they can be tested on real execution traces optimizing the trace analysis. These properties can be designed to test the functional conformance of a protocol as well as security properties. In addition to the theoretical approach, we have developed a software tool that implements the algorithms presented in this paper. Finally, as a proof of concept of our approach and tool we have applied the techniques to two real-life case studies: the SIP and Bluetooth protocol

This dissertation introduces Pikse, a novel methodology for more effective and efficient checking of code conformance to specifications using parallel and incremental techniques, describes a prototype implementation that embodies the methodology, and presents experiments that demonstrate its efficacy. Pikse has at its foundation a well-studied approach -- systematic constraint-driven analysis -- that has two common forms: (1) constraint-based testing -- where logical constraints that define desired inputs and expected program behavior are used for test input generation and correctness checking, say to perform black-box testing; and (2) symbolic execution -- where a systematic exploration of (bounded) program paths using symbolic input values is used to check properties of program behavior, say to perform white-box testing. Our insight at the heart of Pikse is that for certain path-based analyses, (1) the state of a run of the analysis can be encoded compactly, which provides a basis for parallel techniques that have low communication overhead; and (2) iterations performed by the analysis have commonalities, which provides the basis for incremental techniques that re-use results of computations common to successive iterations. We embody our insight into a suite of parallel and incremental techniques that enable more effective and efficient constraint-driven analysis. Moreover, our techniques work in tandem, for example, for combined black-box constraint-based input generation with white-box symbolic execution. We present a series of experiments to evaluate our techniques. Experimental results show Pikse enables significant speedups over previous state-of-the-art. / text

Programinės įrangos testavimas ir kokybės užtikrinimas yra svarbus programų sistemų inžinerijos kūrimo uždavinys, siekiant sukurti tinkamą naudojimui produktą. Yra daug skirtingų metodikų kuriamai programinei įrangai testuoti, tačiau vieningos sistemos, kuri būtų universali – nėra. Įvairūs tyrimai vykdomi programinės įrangos testavimo srityje duoda skirtingus rezultatus. Testavimo procesas taip pat svarbus ir praktikoje – be jo negali išsiversti nei vienas organizacija susijusi su programinės įrangos kūrimu ir plėtojimu. Šis darbas remiasi modeliu paremto testavimo paradigma ir simboliniu vykdymo metodika. Darbe apžvelgiamos teorinės simbolinio vykdymo galimybės, jo pritaikymas .Net platformoje ir papildomos priemonės, kurios reikalingos įgyvendinti tokią sistemą. Taip pat trumpai pristatomas magistro projektinis darbas, aprašomi sukurti inžinerinio produkto svarbiausi aspektai. Pagal teorinę medžiaga sukurtas simbolinio vykdymo variklis – Symex. Darbe nagrinėjamas praktinis tokio įrankio pritaikymas generuojant vienetų testus iš išeities kodo – eksperimentiškai tiriamos ir lyginamos simbolinio vykdymo ir atsitiktinių įėjimų vienetų testų kūrimo galimybės .Net platformoje. / Testing complex safety critical software always was difficult task. Development of automated techniques for error detection is even more difficult. Well known techniques for checking software are model checking static analysis and testing. Symbolic execution is a technique that is being used to improve security, to find bugs, and to help in debugging. A symbolic execution engine is basically an interpreter that figures out how to follow all paths in a program. It is a static code analysis technique. This work presents symbolic execution background, current state, analysis the possibilities of implementation on the .Net framework and platform. The work describes the master project – bug tracking software “Crunchbug” and the tool – Symex (symbolic execution engine) for .Net platform. Symex is white box model based automatic unit test generator and it is evaluated against two other tools – Microsoft Pex and framework that generates unit test inputs random. Detailed experiments made to cover symbolic execution possibilities with proprietary benchmarks and real code from the master project.

Due to the increasing complexity of reactive systems, testing has become an important part in the process of the development of such systems. Conformance testing with formal methods refers to checking functional correctness, by means of testing, of a black-box system under test with respect to a formal system specification, i.e., a specification given in a language with a formal semantics. In this aspect, passive testing techniques are used when the implementation under test cannot be disturbed or the system interface is not provided. Passive testing techniques are based on the observation and verification of properties on the behavior of a system without interfering with its normal operation, it also helps to observe abnormal behavior in the implementation under test on the basis of observing any deviation from the predefined behavior. The main objective of this thesis is to present a new approach to perform passive testing based on the analysis of the control and data part of the system under test. During the last decades, many theories and tools have been developed to perform conformance testing. However, in these theories, the specifications or properties of reactive systems are often modeled by different variants of Labeled Transition Systems (LTS). However, these methodologies do not explicitly take into account the system's data, since the underlying model of LTS are not able to do that. Hence, it is mandatory to enumerate the values of the data before modeling the system. This often results in the state-space explosion problem. To overcome this limitation, we have studied a model called Input-Output Symbolic Transition Systems (IOSTS) which explicitly includes all the data of a reactive system. Many passive testing techniques consider only the control part of the system and neglect data, or are confronted with an overwhelming amount of data values to process. In our approach, we consider control and data parts by integrating the concepts of symbolic execution and we improve trace analysis by introducing trace slicing techniques. Properties are described using Input Output Symbolic Transition Systems (IOSTSs) and we illustrate in our approach how they can be tested on real execution traces optimizing the trace analysis. These properties can be designed to test the functional conformance of a protocol as well as security properties. In addition to the theoretical approach, we have developed a software tool that implements the algorithms presented in this paper. Finally, as a proof of concept of our approach and tool we have applied the techniques to two real-life case studies: the SIP and Bluetooth protocol

On est habitué à penser comme suit à un programme qui exécute: une donnée entre (un input), un moment passe, et un résultat ressort. On assume tacitement de l'information complète sur le input, le résultat, et n'importe quels résultats intermédiaires. Dans ce travail-ci, on demande ce que ça voudrait dire d'exécuter un programme sur de l'information partielle. Comme réponse possible, on introduit l'interprétation partielle, notre contribution principale. Au lieu de considérer un seul input, on considère un ensemble de inputs possibles. Au lieu de calculer un seul résultat, on calcule un ensemble de résultats possibles, et des ensembles de résultats intermédiaires possibles. On approche l'interprétation partielle à partir du problème de la spécialisation de programme: l'optimisation d'un programme pour certains inputs. Faire ça automatiquement porte historiquement le nom d'évaluation partielle. Ç'a été appliqué avec succès à plusieurs problèmes spécifiques. On croit que ça devrait être un outil de programmation commun, pour spécialiser des librairies générales pour usage spécifique - mais ce n'est pas le cas. Souvent, une implantation donnée de l'évaluation partielle ne fonctionne pas uniformément bien sur tous les programmes. Ça se prête mal à un usage commun. On voit ce manque de régularité comme un problème de précision: si l'évaluateur partiel était très précis, il trouverait la bonne spécialisation, indépendamment de notre style de programme. On propose donc une approche de principe à l'évaluation partielle, visant la précision complète, retirée d'exemples particuliers. On reformule l'évaluation partielle pour la baser sur l'interprétation partielle: le calcul sur de l'information partielle. Si on peut déterminer ce qu'on sait sur chaque donnée dans le programme, on peut décider quelles opérations peuvent être éliminées pour spécialiser le programme: les opérations dont le résultat est unique. On définit une représentation d'ensembles qui ressemble à la définition en compréhension, en mathématiques. On modifie un interpréteur pour des programmes fonctionnels, pour qu'il calcule sur ces ensembles. On utilise un solver SMT pour réaliser les opérations sur les ensembles. Pour assurer la terminaison de l'interpréteur modifié, on applique des idées de l'interprétation abstraite: le calcul de point fixe, et le widening. Notre implantation initiale produit de bons résultats, mais elle est lente pour de plus gros exemples. On montre comment l'accélérer mille fois, en dépendant moins de SMT. / We are used to the following picture of an executing program: an input is provided, the program runs for a while, and a result comes out. We tacitly assume complete information about the input, the result, and any intermediate results in between. In this work, we ask what it would mean to execute a program over partial information. As a possible answer, we introduce partial interpretation, our main contribution. Instead of considering a unique input, we consider a set of possible inputs. Instead of computing a unique result, we compute a set of possible results, and sets of possible intermediate results. We approach partial interpretation from the problem of program specialization: the optimization of a program's execution time for certain inputs. Doing this automatically is historically known as partial evaluation. Partial evaluation has been applied successfully to many specific problems. We believe it should be a mainstream programming tool, to specialize general libraries for specific use - but such a tool has not been delivered. One common problem is that a given implementation of partial evaluation is inconsistent: it does not work uniformly well on all input programs. This inconsistency makes it unsuited for mainstream use. We view this inconsistency as an accuracy problem: if the partial evaluator was very accurate, it would find the correct specialization, no matter how we present the input program. We therefore propose a principled approach to partial evaluation, aimed at complete accuracy, removed from any particular example program. We reformulate partial evaluation to root it in partial interpretation: computation over partial information. If we can determine what we know about every piece of data in the program, we can decide which operations can be removed to specialize the program: those operations whose result is uniquely known. We represent sets with a kind of mathematical set comprehension. We modify an interpreter for functional programs, to compute over these sets. We use an SMT solver (Satisfiability Modulo Theories) to perform set operations. To ensure termination of the modified interpreter, we apply ideas from abstract interpretation: fixed point computation, and widening. Our initial implementation produces good results, but it is slow for larger examples. We show how to speed it up a thousandfold, by relying less on SMT.