Machine learning models have become increasingly popular in recent years, and not without reason. They enable software to become more powerful, and with less human involvement. As a consequence however, the actions of the software are hard for a human to understand and anticipate. This prohibits the use of machine learning in systems where safety has to be assured, typically using formal proofs of relevant properties. This thesis is focused on robustness - one of many properties that can impact the safety of a system. There are several tools available that enable formal robustness verification of machine learning models, and a goal of this thesis is to evaluate their performance. A variety of machine learning models are also assessed according to how robust they can be proved to be. A digit recognition problem was used in order to evaluate how sensitive different model types are to perturbations of pixels in an image, and also to assess the performance of applicable verification tools. On this particular problem, we discovered that a Support Vector Machine demonstrates the highest degree of robustness, which could be verified with short enough time using the tool SAVer. In addition, machine learning models were trained on a data set consisting of Android applications that are labelled either as malware or benign. In this verification problem, we check whether adding permission requests to an application that is malware can make it become labelled as benign. For this problem, a Gradient Boosting Machine proved to be the most robust with a very short verification time using the tool VoTE. Although not the most robust, Neural Networks were proved to be relatively robust on both problems using the tool ERAN, whereas Random Forests performed the worst, in terms of robustness.

Formal system modeling has been a topic of interest in the research community for many years. Modeling a system helps engineers understand it better and enables them to check different aspects of it to ensure that there is no undesired or unexpected behavior and that it does what it was designed to do. This thesis takes two existing tools that were created to aid in the designing of spacecraft systems and creates a layer to connect them together and allow them to be used jointly. The first tool is a library of formal descriptions used to specify spacecraft behavior in an unambiguous manner. The second tool is a graphical modeling language that allows a designer to create a model using traditional block diagram descriptions. These block diagrams can be translated to the formal descriptions using the layer created as part of this thesis work. The software of a small satellite, and the additions made to it as part of this thesis work, is also described. Approaches to modeling this software formally are discussed, as are the problems that were encountered that led to expansions of the formal description library to allow better system description.

À mesure que le nombre d’objets capables de communiquer croît, le besoin de sécuriser leurs interactions également. La conception des protocoles cryptographiques nécessaires pour cela est une tâche notoirement complexe et fréquemment sujette aux erreurs humaines. La vérification formelle de protocoles entend offrir des méthodes automatiques et exactes pour s’assurer de leur sécurité. Nous nous intéressons en particulier aux méthodes de vérification automatique des propriétés d’équivalence pour de tels protocoles dans le modèle symbolique et pour un nombre non borné de sessions. Les propriétés d’équivalences ont naturellement employées pour s’assurer, par exemple, de l’anonymat du vote électronique ou de la non-traçabilité des passeports électroniques. Parce que la vérification de propriétés d’équivalence est un problème complexe, nous proposons dans un premier temps deux méthodes pour en simplifier la vérification : tout d’abord une méthode pour supprimer l’utilisation des nonces dans un protocole tout en préservant la correction de la vérification automatique; puis nous démontrons un résultat de typage qui permet de restreindre l’espace de recherche d’attaques sans pour autant affecter le pouvoir de l’attaquant. Dans un second temps nous exposons trois classes de protocoles pour lesquelles la vérification de l’équivalence dans le modèle symbolique est décidable. Ces classes bénéficient des méthodes de simplification présentées plus tôt et permettent d’étudier automatiquement des protocoles taggués, avec ou sans nonces, ou encore des protocoles ping-pong. / As the number of devices able to communicate grows, so does the need to secure their interactions. The design of cryptographic protocols is a difficult task and prone to human errors. Formal verification of such protocols offers a way to automatically and exactly prove their security. In particular, we focus on automated verification methods to prove the equivalence of cryptographic protocols for a un-bounded number of sessions. This kind of property naturally arises when dealing with the anonymity of electronic votingor the untracability of electronic passports. Because the verification of equivalence properties is a complex issue, we first propose two methods to simplify it: first we design a transformation on protocols to delete any nonce while maintaining the soundness of equivalence checking; then we prove a typing result which decreases the search space for attacks without affecting the power of the attacker. Finally, we describe three classes of protocols for which equivalence is decidable in the symbolic model. These classes benefit from the simplification results stated earlier and enable us to automatically analyze tagged protocols with or without nonces, as well as ping-pong protocols.

Při vývoji současných číslicových systémů, např. vestavěných systému a počítačového hardware, je nutné hledat postupy, jak zvýšit jejich spolehlivost. Jednou z možností je zvyšování efektivity a rychlosti verifikačních procesů, které se provádějí v raných fázích návrhu. V této dizertační práci se pozornost věnuje verifikačnímu přístupu s názvem funkční verifikace. Je identifikováno několik výzev a problému týkajících se efektivity a rychlosti funkční verifikace a ty jsou následně řešeny v cílech dizertační práce. První cíl se zaměřuje na redukci simulačního času v průběhu verifikace komplexních systémů. Důvodem je, že simulace inherentně paralelního hardwarového systému trvá velmi dlouho v porovnání s během v skutečném hardware. Je proto navrhnuta optimalizační technika, která umisťuje verifikovaný systém do FPGA akcelerátoru, zatím co část verifikačního prostředí stále běží v simulaci. Tímto přemístěním je možné výrazně zredukovat simulační režii. Druhý cíl se zabývá ručně připravovanými verifikačními prostředími, která představují výrazné omezení ve verifikační produktivitě. Tato režie však není nutná, protože většina verifikačních prostředí má velice podobnou strukturu, jelikož využívají komponenty standardních verifikačních metodik. Tyto komponenty se jen upravují s ohledem na verifikovaný systém. Proto druhá optimalizační technika analyzuje popis systému na vyšší úrovni abstrakce a automatizuje tvorbu verifikačních prostředí tím, že je automaticky generuje z tohoto vysoko-úrovňového popisu. Třetí cíl zkoumá, jak je možné docílit úplnost verifikace pomocí inteligentní automatizace. Úplnost verifikace se typicky měří pomocí různých metrik pokrytí a verifikace je ukončena, když je dosažena právě vysoká úroveň pokrytí. Proto je navržena třetí optimalizační technika, která řídí generování vstupů pro verifikovaný systém tak, aby tyto vstupy aktivovali současně co nejvíc bodů pokrytí a aby byla rychlost konvergence k maximálnímu pokrytí co nejvyšší. Jako hlavní optimalizační prostředek se používá genetický algoritmus, který je přizpůsoben pro funkční verifikaci a jeho parametry jsou vyladěny pro tuto doménu. Běží na pozadí verifikačního procesu, analyzuje dosažené pokrytí a na základě toho dynamicky upravuje omezující podmínky pro generátor vstupů. Tyto podmínky jsou reprezentovány pravděpodobnostmi, které určují výběr vhodných hodnot ze vstupní domény. Čtvrtý cíl diskutuje, zda je možné znovu použít vstupy z funkční verifikace pro účely regresního testování a optimalizovat je tak, aby byla rychlost testování co nejvyšší. Ve funkční verifikaci je totiž běžné, že vstupy jsou značně redundantní, jelikož jsou produkovány generátorem. Pro regresní testy ale tato redundance není potřebná a proto může být eliminována. Zároveň je ale nutné dbát na to, aby úroveň pokrytí dosáhnutá optimalizovanou sadou byla stejná, jako u té původní. Čtvrtá optimalizační technika toto reflektuje a opět používá genetický algoritmus jako optimalizační prostředek. Tentokrát ale není integrován do procesu verifikace, ale je použit až po její ukončení. Velmi rychle odstraňuje redundanci z původní sady vstupů a výsledná doba simulace je tak značně optimalizována.

京都大学 / 0048 / 新制・課程博士 / 博士(工学) / 甲第19309号 / 工博第4106号 / 新制||工||1633(附属図書館) / 32311 / 京都大学大学院工学研究科電気工学専攻 / (主査)教授 引原 隆士, 准教授 三谷 友彦, 教授 岡部 寿男, 教授 土居 伸二, / 学位規則第4条第1項該当 / Doctor of Philosophy (Engineering) / Kyoto University / DFAM

© 2015 Springer. http://dx.doi.org/10.1007/978-3-319-26529-2_11© 2015 ACM, Inc. http://doi.acm.org/10.1145/2676726.2676996 / 京都大学 / 0048 / 新制・課程博士 / 博士(情報学) / 甲第19863号 / 情博第614号 / 新制||情||107(附属図書館) / 32899 / 京都大学大学院情報学研究科通信情報システム専攻 / (主査)教授 五十嵐 淳, 教授 山本 章博, 教授 岡部 寿男 / 学位規則第4条第1項該当 / Doctor of Informatics / Kyoto University / DFAM

No description available.

Continuum robots mimic the principle of a special biological structure known as the muscular hydrostat. These robots have an ability to bend at any location on along its backbone and have potential applications in disaster relief, medical surgeries and nuclear waste disposal. This thesis presents the modeling and verification of a multi-section continuum robot by applying the Cosserat theory of rods. Next, 2D verification is performed on a continuum robot based on a backbone composed of a nickel titanium alloy. In addition, the thesis develops the theoretical foundations for a cable-driven continuum robot by studying the effects of cable guide mass which cause additional deformation of the robot The results of this thesis show that the multi-section model is accurate within 3.4% in predicting the Cartesian tip coordinates, and the model with the cable guides accurate within 1.26% error in predicted versus the observed Cartesian tip coordinates of the backbone.

No description available.

State exploration in directed software model checking is guided using a heuristic function to move states near errors to the front of the search queue. Distance heuristic functions rank states based on the number of transitions needed to move the current program state into an error location. Lack of calling context information causes the heuristic function to underestimate the true distance to the error; however, inlining functions at call sites in the control flow graph to capture calling context leads to exponential growth in the computation. This paper presents a new algorithm that implicitly inlines functions at call sites to compute distance data with unbounded calling context that is polynomial in the number of nodes in the control flow graph. The new algorithm propagates distance data through call sites during a depth-first traversal of the program. We show in a series of benchmark examples that the new heuristic function with unbounded distance data is more efficient than the same heuristic function that inlines functions up to a certain depth.