Nesta tese apresentamos o projeto e a implementação do KEMS, um provador de teoremas multi-estratégia baseado no método de tablôs KE. Um provador de teoremas multi-estratégia é um provador de teoremas onde podemos variar as estratégias utilizadas sem modificar o núcleo da implementação. Além de multi-estratégia, o KEMS é capaz de provar teoremas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi. Listamos abaixo algumas das contribuições deste trabalho: * um sistema KE para mbC que é analítico, correto e completo; * um sistema KE para mCi que é correto e completo; * um provador de teoremas multi-estratégia com as seguintes características: - aceita problemas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi; - tem seis estratégias implementadas para lógica clássica proposicional, duas para mbC e duas para mCi; - tem treze ordenadores que são usados em conjunto com as estratégias; - implementa regras simplificadoras para lógica clássica proposicional; - possui uma interface gráfica que permite a visualização de provas; - é de código aberto e está disponível na Internet em http://kems.iv.fapesp.br; * benchmarks obtidos através da comparação das estratégias para lógica clássica proposicional resolvendo várias famílias de problemas; - sete famílias de problemas para avaliar provadores de teoremas paraconsistentes; * os primeiros benchmarks para as famílias de problemas para avaliar provadores de teoremas paraconsistentes. / In this thesis we present the design and implementation of KEMS, a multi-strategy theorem prover based on the KE tableau inference system. A multi-strategy theorem prover is a theorem prover where we can vary the strategy without modifying the core of the implementation. Besides being multi-strategy, KEMS is capable of proving theorems in three logical systems: classical propositional logic, mbC and mCi. We list below some of the contributions of this work: * an analytic, correct and complete KE system for mbC; * a correct and complete KE system for mCi; * a multi-strategy prover with the following characteristics: - accepts problems in three logical systems: classical propositional logic, mbC and mCi; - has 6 implemented strategies for classical propositional logic, 2 for mbC and 2 for mCi; - has 13 sorters to be used alongside with the strategies; - implements simplification rules of classical propositional logic; - provides a proof viewer with a graphical user interface; - it is open source and available on the internet at http://kems.iv.fapesp.br; * benchmark results obtained by KEMS comparing its classical propositional logic strategies with several problem families; * seven problem families designed to evaluate provers for logics of formal inconsistency; * the first benchmark results for the problem families designed to evaluate provers for logics of formal inconsistency.

This thesis will cover the topic of cyber security in vehicles. Current vehicles contain many computers which communicate over a controller area network. This network has many vulnerabilities which can be leveraged by attackers. To combat these attackers, intrusion detection systems have been implemented. The latest research has mostly focused on the use of deep learning techniques for these intrusion detection systems. However, these deep learning techniques are not foolproof and possess their own security vulnerabilities. One such vulnerability comes in the form of adversarial samples. These are attacks that are manipulated to evade detection by these intrusion detection systems. In this thesis, the aim is to show that the known vulnerabilities of deep learning techniques are also present in the current state-of-the-art intrusion detection systems. The presence of these vulnerabilities shows that these deep learning based systems are still to immature to be deployed in actual vehicles. Since if an attacker is able to use these weaknesses to circumvent the intrusion detection system, they can still control many parts of the vehicles such as the windows, the brakes and even the engine. Current research regarding deep learning weaknesses has mainly focused on the image recognition domain. Relatively little research has investigated the influence of these weaknesses for intrusion detection, especially on vehicle networks. To show these weaknesses, firstly two baseline deep learning intrusion detection systems were created. Additionally, two state-of-the-art systems from recent research papers were recreated. Afterwards, adversarial samples were generated using the fast gradient-sign method on one of the baseline systems. These adversarial samples were then used to show the drop in performance of all systems. The thesis shows that the adversarial samples negatively impact the two baseline models and one state-of-the-art model. The state-of-the-art model’s drop in performance goes as high as 60% in the f1-score. Additionally, some of the adversarial samples need as little as 2 bits to be changed in order to evade the intrusion detection systems. / Detta examensarbete kommer att täcka ämnet cybersäkerhet i fordon. Nuvarande fordon innehåller många datorer som kommunicerar över ett så kallat controller area network. Detta nätverk har många sårbarheter som kan utnyttjas av angripare. För att bekämpa dessa angripare har intrångsdetekteringssystem implementerats. Den senaste forskningen har mestadels fokuserat på användningen av djupinlärningstekniker för dessa intrångsdetekteringssystem. Dessa djupinlärningstekniker är dock inte idiotsäkra och har sina egna säkerhetsbrister. En sådan sårbarhet kommer i form av kontradiktoriska prover. Dessa är attacker som manipuleras för att undvika upptäckt av dessa intrångsdetekteringssystem. I det här examensarbetet kommer vi att försöka visa att de kända sårbarheterna hos tekniker för djupinlärning också finns i de nuvarande toppmoderna systemen för intrångsdetektering. Förekomsten av dessa sårbarheter visar att dessa djupinlärningsbaserade system fortfarande är för omogna för att kunna användas i verkliga fordon. Eftersom om en angripare kan använda dessa svagheter för att kringgå intrångsdetekteringssystemet, kan de fortfarande kontrollera många delar av fordonet som rutorna, bromsarna och till och med motorn. Aktuell forskning om svagheter i djupinlärning har främst fokuserat på bildigenkänningsdomänen. Relativt lite forskning har undersökt inverkan av dessa svagheter för intrångsdetektering, särskilt på fordonsnätverk. För att visa dessa svagheter skapades först två baslinjesystem för djupinlärning intrångsdetektering. Dessutom återskapades två toppmoderna system från nya forskningsartiklar. Efteråt genererades motstridiga prover med hjälp av den snabba gradient-teckenmetoden på ett av baslinjesystemen. Dessa kontradiktoriska prover användes sedan för att visa nedgången i prestanda för alla system. Avhandlingen visar att de kontradiktoriska proverna negativt påverkar de två baslinjemodellerna och en toppmodern modell. Den toppmoderna modellens minskning av prestanda går så högt som 60% i f1-poängen. Dessutom behöver några av de kontradiktoriska samplen så lite som 2 bitar att ändras för att undvika intrångsdetekteringssystem.

In this work, we set the stage of a limited labelling budget and propose using a sample selector network to learn and select effective training samples, whose labels we would then acquire to train the target model performing the required machine learning task. We make the assumption that the sample features, the state of the target model and the training loss of the target model are informative for training the sample selector network. In addition, we approximate the state of the target model with its intermediate and final network outputs. We investigate if under a limited labelling budget, the sample selector network is capable of learning and selecting training samples that train the target model at least as effectively as using another training subset of the same size that is uniformly randomly sampled from the full training dataset, the latter being the common procedure used to train machine learning models without active learning. We refer to this common procedure as the traditional machine learning uniform random sampling method. We perform experiments on the MNIST and CIFAR-10 datasets; and demonstrate with empirical evidence that under a constrained labelling budget and some other conditions, active learning using a sample selector network enables the target model to learn more effectively. / I detta arbete sätter vi steget i en begränsad märkningsbudget och föreslår att vi använder ett provväljarnätverk för att lära och välja effektiva träningsprover, vars etiketter vi sedan skulle skaffa för att träna målmodellen som utför den nödvändiga maskininlärningsuppgiften. Vi antar att provfunktionerna, tillståndet för målmodellen och utbildningsförlusten för målmodellen är informativa för att träna provväljarnätverket. Dessutom uppskattar vi målmodellens tillstånd med dess mellanliggande och slutliga nätverksutgångar. Vi undersöker om provväljarnätverket enligt en begränsad märkningsbudget kan lära sig och välja utbildningsprover som tränar målmodellen minst lika effektivt som att använda en annan träningsdel av samma storlek som är enhetligt slumpmässigt samplad från hela utbildningsdatasystemet, det senare är det vanliga förfarandet som används för att utbilda maskininlärningsmodeller utan aktivt lärande. Vi hänvisar till denna vanliga procedur som den traditionella maskininlärning enhetliga slumpmässig sampling metod. Vi utför experiment på datasätten MNIST och CIFAR-10; och visa med empiriska bevis att under en begränsad märkningsbudget och vissa andra förhållanden, aktivt lärande med hjälp av ett provvalnätverk gör det möjligt för målmodellen att lära sig mer effektivt.

Formal verification of programs can be done with the aid of an interactive theorem prover. The program to be verified is represented in an intermediate language representation inside the interactive theorem prover, after which statements and their proofs can be constructed. This is a process that can be automated to a high degree. This thesis presents a proof procedure to efficiently generate a theorem stating the weakest precondition for a program to terminate successfully in a state upon which a certain postcondition is placed. Specifically, the Poly/ML implementation of the SML metalanguage is used to generate a theorem in the HOL4 interactive theorem prover regarding the properties of a program written in BIR, an abstract intermediate representation of machine code used in the PROSPER project. / Bevis av säkerhetsegenskaper hos program genom formell verifiering kan göras med hjälp av interaktiva teorembevisare. Det program som skall verifieras representeras i en mellanliggande språkrepresentation inuti den interaktiva teorembevisaren, varefter påståenden kan konstrueras, som sedan bevisas. Detta är en process som kan automatiseras i hög grad. Här presenterar vi en metod för att effektivt skapa och bevisa ett teorem som visar sundheten hos den svagaste förutsättningen för att ett program avslutas framgångsrikt under ett givet postvillkor. Specifikt använder vi Poly/ML-implementationen av SML för att generera ett teorem i den interaktiva teorembevisaren HOL4 som beskriver egenskaper hos ett program i BIR, en abstrakt mellanrepresentation av maskinkod som används i PROSPER-projektet.

Depuis l’introduction de la mécanique quantique, plusieurs mystères de la nature ont trouvé leurs explications. De plus en plus, les concepts de la mécanique quantique se sont entremêlés avec d’autres de la théorie de la complexité du calcul. De nouvelles idées et solutions ont été découvertes et élaborées dans le but de résoudre ces problèmes informatiques. En particulier, la mécanique quantique a secoué plusieurs preuves de sécurité de protocoles classiques. Dans ce m´emoire, nous faisons un étalage de résultats récents de l’implication de la mécanique quantique sur la complexité du calcul, et cela plus précisément dans le cas de classes avec interaction. Nous présentons ces travaux de recherches avec la nomenclature des jeux à information imparfaite avec coopération. Nous exposons les différences entre les théories classiques, quantiques et non-signalantes et les démontrons par l’exemple du jeu à cycle impair. Nous centralisons notre attention autour de deux grands thèmes : l’effet sur un jeu de l’ajout de joueurs et de la répétition parallèle. Nous observons que l’effet de ces modifications a des conséquences très différentes en fonction de la théorie physique considérée. / Since the introduction of quantum mechanics, many mysteries of nature have found explanations. Many quantum-mechanical concepts have merged with the field of computational complexity theory. New ideas and solutions have been put forward to solve computational problems. In particular, quantum mechanics has struck down many security proofs of classical protocols. In this thesis, we survey recent results regarding the implication of quantum mechanics to computational complexity and more precisely to classes with interaction. We present the work done in the framework of cooperative games with imperfect information. We give some differences between classical, quantum and no-signaling theories and apply them to the specific example of Odd Cycle Games. We center our attention on two different themes: the effect on a game of adding more players and of parallel repetition. We observe that depending of the physical theory considered, the consequences of these changes is very different.

Les travaux présentés dans cette thèse proposent une méthode de génération automatique de tests à partir de modèles.Cette méthode emploie deux langages de modélisations UML4MBT et OCL4MBT qui ont été spécifiquement dérivées d’ UML et OCL pour la génération de tests. Ainsi les comportements, la structure et l’état initial du système sont décrits au travers des diagrammes de classes, d’objets et d’états-transitions.Pour générer des tests, l’évolution du modèle est représente sous la forme d’un système de transitions. Ainsi la construction de tests est équivalente à la découverte de séquences de transitions qui relient l’´état initial du système à des états validant les cibles de test.Ces séquences sont obtenues par la résolution de scénarios d’animations par des prouveurs SMT et solveurs CSP. Pour créer ces scénarios, des méta-modèles UML4MBT et CSP4MBT regroupant formules logiques et notions liées aux tests ont été établies pour chacun des outils.Afin d’optimiser les temps de générations, des stratégies ont été développé pour sélectionner et hiérarchiser les scénarios à résoudre. Ces stratégies s’appuient sur la parallélisation, les propriétés des solveurs et des prouveurs et les caractéristiques de nos encodages pour optimiser les performances. 5 stratégies emploient uniquement un prouveur et 2 stratégies reposent sur une collaboration du prouveur avec un solveur.Finalement l’intérêt de cette nouvelle méthode à été validée sur des cas d’études grâce à l’implémentation réalisée. / This thesis describes an automatic test generation process from models.This process uses two modelling languages, UML4MBT and OCL4MBT, created specificallyfor tests generation. Theses languages are derived from UML and OCL. Therefore the behaviours,the structure and the initial state of the system are described by the class diagram, the objectdiagram and the state-chart.To generate tests, the evolution of the model is encoded with a transition system. Consequently,to construct a test is to find transition sequences that rely the initial state of the system to thestates described by the test targets.The sequence are obtained by the resolution of animation scenarios. This resolution is executedby SMT provers and CSP solvers. To create the scenario, two dedicated meta-models, UML4MBTand CSP4MBT have been established. Theses meta-models associate first order logic formulas withthe test notions.7 strategies have been developed to improve the tests generation time. A strategy is responsiblefor the selection and the prioritization of the scenarios. A strategy is built upon the properties ofthe solvers and provers and the specification of our encoding process. Moreover the process canalso be paralleled to get better performance. 5 strategies employ only a prover and 2 make theprover collaborate with a solver.Finally the interest of this process has been evaluated through a list of benchmark on variouscases studies.

No description available.

<p>In this thesis, porous graphitic carbon (PGC) has been used as packing material in packed capillary liquid chromatography. The unique chromatographic properties of PGC has been studied in some detail and applied to different analytical challenges using both electrospray ionization-mass spectrometry (ESI-MS) and ultra violet (UV) absorbance detection. </p><p>The crucial importance of disengaging the conductive PGC chromatographic separation media from the high voltage mass spectrometric interface has been shown. In the absence of a grounded point between the column and ESI emitter, a current through the column was present, and changed retention behaviors for 3-O-methyl-DOPA and tyrosine were observed. An alteration of the chromatographic properties was also seen when PGC was chemically oxidized with permanganate, possibly due to an oxidation of the few surface groups present on the PGC material. </p><p>The dynamic adsorption of the chiral selector lasalocid onto the PGC support resulted in a useful and stable chiral stationary phase. Extraordinary enantioselectivity was observed for 1-(1-naphthyl)ethylamine, and enantioseparation was also achieved for other amines, amino acids, acids and alcohols. </p><p>Finally, a new strategy for separation of small biologically active compounds in plasma and brain tissue has been developed. With PGC as stationary phase it was possible to utilize a mobile phase of high content of organic modifier, without the addition of ion-pairing agents, and still selectively separate the analytes. </p>

In this thesis, porous graphitic carbon (PGC) has been used as packing material in packed capillary liquid chromatography. The unique chromatographic properties of PGC has been studied in some detail and applied to different analytical challenges using both electrospray ionization-mass spectrometry (ESI-MS) and ultra violet (UV) absorbance detection. The crucial importance of disengaging the conductive PGC chromatographic separation media from the high voltage mass spectrometric interface has been shown. In the absence of a grounded point between the column and ESI emitter, a current through the column was present, and changed retention behaviors for 3-O-methyl-DOPA and tyrosine were observed. An alteration of the chromatographic properties was also seen when PGC was chemically oxidized with permanganate, possibly due to an oxidation of the few surface groups present on the PGC material. The dynamic adsorption of the chiral selector lasalocid onto the PGC support resulted in a useful and stable chiral stationary phase. Extraordinary enantioselectivity was observed for 1-(1-naphthyl)ethylamine, and enantioseparation was also achieved for other amines, amino acids, acids and alcohols. Finally, a new strategy for separation of small biologically active compounds in plasma and brain tissue has been developed. With PGC as stationary phase it was possible to utilize a mobile phase of high content of organic modifier, without the addition of ion-pairing agents, and still selectively separate the analytes.