Programmers often have to spend a significant amount of time inspecting the software code and execution traces to identify the root cause of a software bug. For a multithreaded program, debugging is even more challenging due to the subtle interactions between concurrent threads and the often astronomical number of possible interleavings. In this work, we propose a logical constraint-based symbolic analysis method to aid in the diagnosis of concurrency bugs and find their root causes, which can be later used to recommend repairs. In our method, the diagnosis process is formulated as a set of constraint solving problems. By leveraging the power of constraint satisfiability (SAT) solvers and a bounded model checker, we perform a semantic analysis of the sequential computation as well as the thread interactions. The analysis is ideally suited for handling software with small to medium code size but complex concurrency control, such as device drivers, synchronization protocols, and concurrent data structures. We have implemented our method in a software tool and demonstrated its effectiveness in diagnosing subtle concurrency bugs in multithreaded C programs. / Master of Science

Innovative nano-scale devices have been developed to enhance future circuit design to overcome physical barriers hindering complementary metal-oxide semiconductor (CMOS) technology. Among the emerging nanodevices, resonant tunneling diodes (RTDs) have demonstrated promising electronic features due to their high speed switching capability and functional versatility. Great circuit functionality can be achieved through integrating heterostructure field-effect transistors (HFETs) in conjunction with RTDs to modulate effective negative differential resistance (NDR). However, RTDs are intrinsically suitable for implementing threshold logic rather than Boolean logic which has dominated CMOS technology in the past. To fully take advantage of such emerging nanotechnology, efficient design methodologies and design automation tools for threshold logic therefore become essential. In this thesis, we first propose novel programmable logic elements (PLEs) implemented in threshold gates (TGs) and multi-threshold threshold gates (MTTGs) by exploring RTD/ HFET monostable-bistable transition logic element (MOBILE) principles. Our three-input PLE can be configured through five control bits to realize all the three-variable logic functions, which is, to the best of our knowledge, the first single RTD-based structure that provides complete logic implementation. It is also a more efficient reconfigurable circuit element than a general look-up table which requires eight configuration bits for three-variable functions. We further extend the design concept to construct a more versatile four-input PLE. A comprehensive comparison of three- and four-input PLEs provides an insightful view of design tradeoffs between performance and area. We present the mathematical proof of PLE's logic completeness based on Shannon Expansion, as well as the HSPICE simulation results of the programmable and primitive RTD/HFET gates that we have designed. An efficient control bit generating algorithm is developed by using a special encoding scheme to implement any given logic function. In addition, we propose novel techniques of formulating a given threshold logic in conjunctive normal form (CNF) that facilitates efficient SAT-based equivalence checking for threshold logic networks. Three different strategies of CNF generation from threshold logic representations are implemented. Experimental results based on MCNC benchmarks are presented as a complete comparison. Our hybrid algorithm, which takes into account input symmetry as well as input weight order of threshold gates, can efficiently generate CNF formulas in terms of both SAT solving time and CNF generating time. / Master of Science

As the number of transistors per unit chip area increases, the power dissipation of the chip becomes a bottleneck. New nano-technology materials have been proposed as viable alternatives to CMOS to tackle area and power issues. The power consumption can be minimized by the use of reversible logic instead of conventional combinational circuits. Theoretically, reversible circuits do not consume any power (or consume minimal power) when performing computations. This is achieved by avoiding information loss across the circuit. However, use of reversible circuits to implement digital logic requires development of new Electronic Design Automation techniques. Several approaches have been proposed and each method has its own pros and cons. This often results in multiple designs for the same function. Consequently, this demands research in efficient equivalence checking techniques for reversible circuits. This thesis explores the optimization and equivalence checking of reversible circuits. Most of the existing synthesis techniques work in two steps — generate an original, often sub-optimal, implementation for the circuit followed optimization of this design. This work proposes the use of Binary Decision Diagrams for optimization of reversible circuits. The proposed technique identifies repeated gate (trivial) as well as non-contiguous redundancies in a reversible circuit. Construction of a BDD for a sub-circuit (obtained by sliding a window of fixed size over the circuit) identifies redundant gates based upon the redundant variables in the BDD. This method was unsuccessful in identifying any additional redundancies in benchmark circuits; however, hidden non-contiguous redundancies were consistently identified for a family of randomly generated reversible circuits. As of now, several research groups focus upon efficient synthesis of reversible circuits. However, little work has been done in identification of redundant gates in existing designs and the proposed peephole optimization method stands among the few known techniques. This method fails to identify redundancies in a few cases indicating the complexity of the problem and the need for further research in this area. Even for simple logical functions, multiple circuit representations exist which exhibit a large variation in the total number of gates and circuit structure. It may be advantageous to have multiple implementations to provide flexibility in choice of implementation process but it is necessary to validate the functional equivalence of each such design. Equivalence checking for reversible circuits has been researched to some extent and a few pre-processing techniques have been proposed prior to this work. One such technique involves the use of Reversible Miter circuits followed by SAT-solvers to ascertain equivalence. The second half of this work focuses upon the application of the proposed reduction technique to Reversible Miter circuits as a pre-processing step to improve the efficiency of the subsequent SAT-based equivalence checking. / Master of Science

Programmed Cell Death, or Apoptosis, plays a critical role in human embryonic development and in adult tissue homeostasis. Recent research efforts in Bioinformatics and Computational Biology focus on gaining deep insight into the Apoptosis process. This allows researchers to clearly study the relation between the dysregulation of apoptosis and the development of cancer. Research in this highly interdisciplinary field of bioinformatics has become much more quantitative, using tools from computational sciences to understand the behavior of Biological systems. Previously, an abstracted model has been developed to study the Apoptosis process as a Finite State Discrete Transition Model. This model facilitates the reutilization of the digital design verification and testing techniques developed in the Electronic Design Automation domain. These verification and testing techniques for hardware have become robust over the past few decades. Usually simulation is the cornerstone of the Design Verification industry and bulk of states are covered by simulation. Formal verification techniques are then used to analyze the remaining corner case states. Techniques like Genetic Algorithm guided Logic Simulation (GALS) and SAT-based Induction have already been applied to the Apoptosis Discrete Transition Model. However, the Apoptosis model presents some unique problems. The simulation techniques have shown to be unable to cover most of the states of the Apoptosis model. When SAT-based Induction is applied to the Apoptosis model, in particular to find illegal states, very few illegal states are identified. It particularly suffers from the fact that the Apoptosis Model is rather complex and the formulation for testing and verification is hard to tackle at larger bounds greater than 20 or so. Consequently, the state space of the Apoptosis model largely lies in the unknown region, meaning that we are unable to either reach those states or prove that they are illegal. Unless we know whether these states are reachable or illegal, it is not feasible to infer information about the model such as what protein concentrations can be reached under what kind of input stimuli. Questions such as whether certain protein concentrations can be reached or not in this model can only be answered if we have a clear picture of the reachability of state space. In this thesis, we propose techniques based on ATPG and SAT based image computation of the Apoptosis finite transition model. Our method leverages the results obtained in previous research work. It uses the reachable states obtained from the simulation traces of the previous work as initial states for our technique. This enables us to identify more illegal states in less number of iterations; in other words, we are able to reach the fixed point in image computation faster. Our experimental analysis illustrates that the proposed techniques could prove most of the former unknown states as illegal states. We are able to extend our analysis to obtain clearer picture of the interaction of any two proteins in the system considered together. / Master of Science

Cette thèse aborde le problème de la vérification automatique de systèmesparamétrés complexes. Cette approche est importante car elle permet de garantircertaines propriétés sans connaître a priori le nombre de composants dusystème. On s'intéresse en particulier à la sûreté de ces systèmes et on traitele côté paramétré du problème avec des méthodes symboliques. Ces travauxs'inscrivent dans le cadre théorique du model checking modulo théories et ontdonné lieu à un nouveau model checker : Cubicle.Une des contributions principale de cette thèse est une nouvelle technique pourinférer des invariants de manière automatique. Le processus de générationd'invariants est intégré à l'algorithme de model checking et permet de vérifieren pratique des systèmes hors de portée des approches symboliquestraditionnelles. Une des applications principales de cet algorithme estl’analyse de sûreté paramétrée de protocoles de cohérence de cache de tailleindustrielle.Enfin, pour répondre au problème de la confiance placée dans le model checker,on présente deux techniques de certification de notre outil Cubicle utilisantla plate-forme Why3. La première consiste à générer des certificats dont lavalidité est évaluée de manière indépendante tandis que la seconde est uneapproche par vérification déductive du cœur de Cubicle. / This thesis tackles the problem of automatically verifying complexparameterized systems. This approach is important because it can guarantee thatsome properties hold without knowing a priori the number of components in thesystem. We focus in particular on the safety of such systems and we handle theparameterized aspect with symbolic methods. This work is set in the theoreticalframework of the model checking modulo theories and resulted in a new modelchecker: Cubicle.One of the main contribution of this thesis is a novel technique forautomatically inferring invariants. The process of invariant generation isintegrated with the model checking algorithm and allows the verification inpractice of systems which are out of reach for traditional symbolicapproaches. One successful application of this algorithm is the safety analysisof industrial size parameterized cache coherence protocols.Finally, to address the problem of trusting the answer given by the modelchecker, we present two techniques for certifying our tool Cubicle based on theframework Why3. The first consists in producing certificates whose validity canbe assessed independently while the second is an approach by deductiveverification of the heart of Cubicle.

Devido à alta complexidade dos Sistemas Produtivos, o projeto de sistemas de controle adequados às exigências normativas vinculadas aos processos industriais que são executados, e seu impacto no ser humano e no ambiente demandam a necessidade do desenvolvimento de soluções de controle que sejam seguras e estáveis no sentido de não causar interrupções no processo produtivo e danos ao ser humano e ao meio. Uma abordagem para o desenvolvimento de sistemas que contemplem estes requisitos baseia-se no conceito de Sistemas Instrumentados de Segurança e na aplicação das normas IEC 61508 e IEC 61511. Entretanto, assim como o desenvolvimento de qualquer software, os programas de controle de SIS também estão sujeitos a erros de especificação e projeto, mesmo quando o desenvolvimento é feito conforme os critérios normatizados. Além dos erros de projeto, também deve ser levado em consideração que as camadas de prevenção e mitigação especificadas nas normas podem ser desenvolvidas separadamente e dessa forma podem ocorrer comportamentos não previstos ou indesejáveis quando da operação conjunta delas. Uma das formas para uma melhoria na confiabilidade desses programas e que também é um requerimento pertinente ao ciclo de desenvolvimento de um SIS - de acordo com as normas de segurança IEC 61508 e IEC 61511 - é a aplicação de técnicas de verificação formal dos modelos desses programas de controle bem como o uso de um ambiente unificado para modelagem desses sistemas de controle, onde suas interações possam ser mais bem compreendidas. Atualmente, umas das técnicas mais proeminentes para a verificação de sistemas é o Model Checking, que realiza uma busca exaustiva no espaço de estados de um sistema dirigido por eventos, verificando as propriedades especificadas a partir de proposições estabelecidas em lógica temporal. Para esse trabalho é utilizada a lógica TCTL devido a sua capacidade de expressar propriedades em domínio temporal denso. Como ferramenta computacional será usado o ambiente GHENeSys, que propicia um ambiente unificado para modelagem, simulação e verificação dos sistemas por conjugar os benefícios de rede de Petri para modelagem e as técnicas de Model Checking para verificação de modelos. / Due to the high complexity of the actual Productive Systems, the design of suitable control systems according to the applicable industrial standards, and the possible negative impacts on the human being, on the environment and on equipment, the development of control solutions that are be both secure and stable as some systems have to operate nonstop is much demanded. One approach for the development systems with such requirements is the use of Safety Instrumented Systems complying with the standards IEC 61508 and IEC 61511. However, as on the development of any kind of software, SIS control programs are also prone to specification and design errors, even when the control programs are developed according to the applicable standards. Besides design errors, must be taken into consideration the fact that the SIS prevention and mitigation layers, as prescribed on the standards, can be developed individually and thus presenting unanticipated or undesirable behaviors when operating together. One way to improve the reliability of these control programs, which is also required by the safety standards IEC 61508 and IEC 61511 as part of the SIS development cycle, is the application of formal verification techniques on the control software models. Another way is to use a unified approach for modeling these control systems, and thus having the opportunity to understand their interactions better. Currently, one of the most prominent techniques for the verification of systems is the Model Checking. Such technique performs an exhaustive search in the space state of an event driven system, verifying the properties specified as established propositions in temporal logic. On this work, the TCTL logic is used due its ability to express properties in the dense time domain. As computational tool will be used GHENeSys environment, as it provides a unified environment for modeling, simulating and the verification of systems, which enjoys the benefits of modelling through Petri Nets and Model Checking techniques for formal verification.

Les architectures de systèmes à logiciel posent des défis pour les experts de sécurité. nombreux travaux ont eu pour objectif d’élaborer des solutions théoriques, des guides méthodologiques et des recommandations, pour renforcer la sécurité et protéger ces systèmes.Une solution proposée est d’intégrer des patrons de sécurité comme solutions méthodologiques à adapter aux spécificités des architectures considérées. Une telle solution est considérée fiable si elle résout un problème de sécurité sans affecter les exigences du système.Une fois un modèle d’architecture implante les patrons de sécurisé, il est nécessaire de valider formellement ce nouveau modèle au regard des exigences attendues. Les techniques de model checking permettent cette validation en vérifiant, d’une part, que les propriétés des patrons de sécurité sont respectées et, d’autre part, que les propriétés du modèle initial sont préservées.Dans ce travail de thèse, nous étudions les méthodes et les concepts pour générer des modèles architecturaux respectant des exigences de sécurité spécifiques. Àpartir d’un modèle d’architecture logicielle, d’une politique de sécurité et d’une librairie des patrons de sécurité, nous souhaitons générer une architecture sécurisée. Chaque patron de sécurité est décrit par une description formelle de sa structure et de son comportement, ainsi qu’une description formelle des propriétés de sécurité associées à ce patron.Cette thèse rend compte des travaux sur l’exploitation de techniques de vérification formelle des propriétés, par model-checking. L’idée poursuivie est de pouvoir générer un modèle d’architecture qui implante des patrons de sécurité, et de vérifier que les propriétés de sécurité, comme les exigences de modèle, sont respectées dans l’architecture résultante.En perspective, les résultats de notre travail pourraient s'appliquer à définir une méthodologie pour une meilleure validation de la sécurité des systèmes industriels comme les SCADA. / Software-based architectures pose challenges for security experts. Many studieshave aimed to develop theoretical solutions, methodological guides and recommendations to enhance security and protect these systems.One solution proposed is to integrate security patterns as methodological solutions to adapt to the specificities of the considered architectures. Such a solution is considered reliable if it solves a security problem without affecting systemrequirements. Once an architecture model implements the security patterns, it is necessary to formally validate this new model against the expected requirements. Model checking techniques allow this validation by verifying, on one hand, that theproperties of the security patterns are respected and, on the other hand, that the properties of the initial model are preserved.In this thesis work, we study the methods and concepts to generate architectural models that meet specific security requirements. Starting with a software architecture model, a security policy and a library of security patterns, we want to generate a secure architecture. Each security pattern is described by aformal description of its structure and behavior, as well as a formal description of the security properties associated with that pattern.This thesis reports work on the technical exploitation of formal verification of properties, using model-checking.The idea is to be able to generate an architecture model that implements security patterns, and to verify that the security properties, as well as the model requirements, are respected in the resulting architecture.In perspective, the results of our work could be applied to define a methodology for a better validation of the security of industrial systems like SCADA.

With the growing number of complex requirements for building and facility projects, diverse domain experts iteratively exchange building design and product data during the design, construction, and facility management phases. Such data exchanges, however, frequently involve unintended geometric transformations, inaccurate project requirements, and insufficient syntactic and semantic elements in building model data. To ensure the interoperability of building information models, this dissertation includes an examination of rules categorized from the Precast Concrete Institute model views and a generalization of the rule logic and structures of each rule set. Moreover, rule logic is coded and implemented on modularized validation platforms of a validation tool referred to as the IfcDoc tool, an automated model view documentation and validation application. This dissertation is expected to help domain experts evaluate whether building design data fulfill the data exchange specifications of their domain and the objectives of a proposed project. Furthermore, to identify unreliable and inconsistent IFC mapping procedures of BIM authoring tools, software developers using the proposed approach would implement an automated debugging process in their IFC interfaces according to the specifications of a targeted model view.

La sécurité des Systèmes d’Information (SI) constitue un défi majeur car elle conditionne amplement la future exploitation d’un SI. C’est pourquoi l’étude des vulnérabilités d’un SI dès les phases conceptuelles est cruciale. Il s’agit d’étudier la validation de politiques de sécurité, souvent exprimées par des règles de contrôle d’accès, et d’effectuer des vérifications automatisées sur des modèles afin de garantir une certaine confiance dans le SI avant son opérationnalisation. Notre intérêt porte plus particulièrement sur la détection des vulnérabilités pouvant être exploitées par des utilisateurs internes afin de commettre des attaques, appelées attaques internes, en profitant de leur accès légitime au système. Pour ce faire, nous exploitons des spécifications formelles B générées, par la plateforme B4MSecure, à partir de modèles fonctionnels UML et d’une description Secure UML des règles de contrôle d’accès basées sur les rôles. Ces vulnérabilités étant dues à l’évolution dynamique de l’état fonctionnel du système, nous proposons d’étudier l’atteignabilité des états, dits indésirables, donnant lieu à des attaques potentielles, à partir d’un état normal du système. Les techniques proposées constituent une alternative aux techniques de model-checking. En effet, elles mettent en œuvre une recherche symbolique vers l’arrière fondée sur des approches complémentaires : la preuve et la résolution de contraintes. Ce processus de recherche est entièrement automatisé grâce à notre outil GenISIS qui a montré, sur la base d’études de cas disponibles dans la littérature, sa capacité à retrouver des attaques déjà publiées mais aussi des attaques nouvelles. / The early detection of potential threats during the modelling phase of a Secure Information System (IS) is required because it favours the design of a robust access control policy and the prevention of malicious behaviours during the system execution. This involves studying the validation of access control rules and performing vulnerabilities automated checks before the IS operationalization. We are particularly interested in detecting vulnerabilities that can be exploited by internal trusted users to commit attacks, called insider attacks, by taking advantage of their legitimate access to the system. To do so, we use formal B specifications which are generated by the B4MSecure platform from UML functional models and a SecureUML modelling of role-based access control rules. Since these vulnerabilities are due to the dynamic evolution of the functional state, we propose to study the reachability of someundesirable states starting from a normal state of the system. The proposed techniques are an alternative to model-checking techniques. Indeed, they implement symbolic backward search algorithm based on complementary approaches: proof and constraint solving. This rich technical background allowed the development of the GenISIS tool which automates our approach and which was successfully experimented on several case studies available in the literature. These experiments showed its capability to extract already published attacks but also new attacks.

Při verifikaci programů se snažíme rozhodnout, zda program obsahuje či neobsahuje chyby. Základním předpokladem všech verifikačních postupů je efektivní reprezentace a manipulace se stavy programů. V této práci představujeme techniky pro nalezení nepodstatných informací ve stavech programů a pro jejich odstranění. Tato práce obsahuje redukce vhodné pro explicitní i symbolickou reprezentaci stavů. Naše postupy vhodné pro explicitní reprezentaci byly speciálně navrženy pro vícevláknové programy. Naše analýzy dokáží nalézt takové hodnoty v dynamicky alokovaných objektech, tedy na haldě, které program již nebude v následujících krocích číst. Logické formule v predikátové nebo výrokové logice jsou převažující symbolickou reprezentací množin stavů programu. Craigovy interpolanty jsou jedním z obvyklých postupů pro získání formulí s požadovanými vlastnostmi. V této práci představujeme nový způsob jejich výpočtu, který používá přiřazení proměnných pro zmenšení jejich velikosti. Pomocí přiřazení proměnných můžeme zablokovat ty cesty v programu, které nechceme, aby interpolant bral v potaz a tím zmenšit jejich velikost.