O presente trabalho trata da verificação e design de sistemas complexos, especificamente da verificação de sistemas de tempo real concorrentes e distribuídos. Propõe-se uma técnica enumerativa para a verificação formal de modelos que permite determinar a validade de propriedades quantitativas, além das qualitativas. A técnica proposta separa a construção do espaço de estados dos algoritmos de rotulação das fórmulas temporais, o que possibilita a diminuição da complexidade do processo de verificação, tornando-o viável para aplicações práticas. A técnica proposta foi inicialmente aplicada sobre modelos de redes de Petri temporizadas e depois em uma rede unificada chamada GHENeSys para aproveitar as características de abstração, hierarquia e de elementos de interação chamados pseudo-boxes. A definição da rede GHENeSys foi modificada para permitir a modelagem de sistemas onde os requisitos temporais devem ser expressos através de atrasos e prazos como e o caso dos sistemas de tempo real. A rede suporta ainda mecanismos de refinamento tanto para os elementos ativos quanto os passivos. A demonstração da manutenção de propriedades como invariantes, vivacidade, limitação assim como da validade de fórmulas lógicas no processo de refinamento constitui um aspecto fundamental no projeto de sistemas complexos, e foi portanto revista em detalhes para a rede GHENeSys. Alguns exemplos práticos são apresentados para avaliar o desempenho dos algoritmos e um estudo de caso finaliza a apresentação, onde se pode contrastar os algoritmos propostos com os implementados na ferramenta UPPAAL. / This work deals with the process of design and verification of complex systems, mainly real time, concurrent and distributed systems. An enumerative technique is proposed for model-checking which is capable of determining both quantitative and qualitative properties. The proposed technique detach the algorithm for labeling the formula being checked from the state space construction, allowing a better result in the verification process. This model-checking approach shows itself valuable in practical applications. This approach was first applied to systems modeled by Time Petri Nets and further extended to a unified net called GHENeSys, which includes abstraction and hierarchy concepts as well as elements for data and control interchange, called pseudo-boxes. The GHENeSys definition was modified in order to deal with systems in which temporal requirements can be expressed through delays and deadlines as in the real-time systems. The GHENeSys environment supports a refinement technique applied to both passive and active elements. Net properties like invariants, liveness, boundedness and also the validity of temporal formulas was proved to be maintained through the refinement process if some conditions are satisfied. Such characteristics are useful to deal with complex systems design. Some experiments based on well known academic articles were used to avaliate the performance of the algorithms and a case study is presented in order to compare obtained results with those obtained using the UPPAAL tool.

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.

Submitted by Geyciane Santos (geyciane_thamires@hotmail.com) on 2015-07-23T13:51:53Z No. of bitstreams: 1 Dissertação - Mikhail Yasha Ramalho Gadelha.pdf: 1839545 bytes, checksum: 9f5e7d75af46b461d8ad6837ce6ad0be (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-23T15:49:26Z (GMT) No. of bitstreams: 1 Dissertação - Mikhail Yasha Ramalho Gadelha.pdf: 1839545 bytes, checksum: 9f5e7d75af46b461d8ad6837ce6ad0be (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-23T15:52:49Z (GMT) No. of bitstreams: 1 Dissertação - Mikhail Yasha Ramalho Gadelha.pdf: 1839545 bytes, checksum: 9f5e7d75af46b461d8ad6837ce6ad0be (MD5) / Made available in DSpace on 2015-07-23T15:52:49Z (GMT). No. of bitstreams: 1 Dissertação - Mikhail Yasha Ramalho Gadelha.pdf: 1839545 bytes, checksum: 9f5e7d75af46b461d8ad6837ce6ad0be (MD5) Previous issue date: 2013-12-20 / FAPEAM - Fundação de Amparo à Pesquisa do Estado do Amazonas / The use of embedded systems, computational systems specialized to do a function in larger systems, electronic or mechanical, is growing in the daily life, and it is becoming increasingly important to ensure the robustness of these systems. There are several techniques to ensure that a system is released without error. In particular, formal verification is proving very effective in finding bugs in programs. In this work, we describe the formal verification for C++ Programs and correctness proof by mathematical induction. Both techniques will be developed using the tool Efficient SMT-Based Context-Bounded Model Checker (ESBMC), a model checker based on satisfiability modulo theories and first order logic. The experiments show that the tool can be used to check a wide range of applications, from simple test cases to commercial applications. The tool also proved to be more efficient than other models checkers to verify C++ programs, finding a greater number of bugs, and supporting a larger number of the features that the language C++ has to offer, in addition to being able to prove several properties, using the method of mathematical induction. / A utilização de sistemas embarcados, sistemas computacionais especializados para realizar uma função em sistemas maiores, eletrônicos ou mecânicos, vem crescendo no dia a dia das pessoas, e vem se tornando cada vez mais importante garantir a robustez desses sistemas. Existem diversas técnicas para garantir que um sistema seja lançado sem erros. Em especial, a verificação formal de programas está se mostrando efetiva na busca por falhas. Neste trabalho, serão descritos a verificação formal de programas C++ e a prova de corretude por indução matemática. Ambas as técnicas serão desenvolvidas utilizando a ferramenta Efficient SMTBased Context-Bounded Model Checker (ESBMC), um verificador de modelos que se baseia em teorias de satisfabilidade de fórmulas proposicionais e de lógica de primeira ordem. Os experimentos mostram que a ferramenta pode ser utilizada para verificar uma ampla gama de aplicações, de casos simples à aplicações comerciais. A ferramenta também mostrou-se superior em comparação com outros verificadores na verificação de programas C++, encontrando um maior número de erros e suportando um número superior das funcionalidades que a linguagem C++ tem a oferecer, além de ser capaz de provar diversas propriedades (por exemplo, laços invariantes), utilizando a técnica de indução matemática.

Over the last years, security-kernels have played a promising role in reshaping the landscape of platform security on embedded devices. Security-kernels, such as separation kernels, enable constructing high-assurance mixed-criticality execution platforms on a small TCB, which enforces isolation between components. The reduced TCB  minimizes the system attack surface and facilitates the use of formal methods to ensure the kernel functional correctness and security. In this thesis, we explore various aspects of building a provably secure separation kernel using virtualization technology. We show how the memory management subsystem can be virtualized to enforce isolation of system components. Virtualization is done using direct-paging that enables a guest software to manage its own memory configuration. We demonstrate the soundness of our approach by verifying that the high-level model of the system fulfills the desired security properties. Through refinement, we then propagate these properties (semi-)automatically to the machine-code of the virtualization mechanism. Further, we show how a runtime monitor can be securely deployed alongside a Linux guest on a hypervisor to prevent code injection attacks targeting Linux. The monitor takes advantage of the provided separation to protect itself and to retain a complete view of the guest. Separating components using a low-level software cannot by itself guarantee the system security. Indeed, current processors architecture involves features that can be utilized to violate the isolation of components. We present a new low-noise attack vector constructed by measuring caches effects which is capable of breaching isolation of components and invalidates the verification of a software that has been verified on a memory coherent model. To restore isolation, we provide several countermeasures and propose a methodology to repair the verification by including data-caches in the statement of the top-level security properties of the system. / <p>QC 20170831</p> / PROSPER / HASPOC

[EN] The availability of new processors with more processing power for embedded systems has raised the development of applications that tackle problems of greater complexity. Currently, the embedded applications have more features, and as a consequence, more complexity. For this reason, there exists a growing interest in allowing the secure execution of multiple applications that share a single processor and memory. In this context, partitioned system architectures based on hypervisors have evolved as an adequate solution to build secure systems. One of the main challenges in the construction of secure partitioned systems is the verification of the correct operation of the hypervisor, since, the hypervisor is the critical component on which rests the security of the partitioned system. Traditional approaches for Validation and Verification (V&V), such as testing, inspection and analysis, present limitations for the exhaustive validation and verification of the system operation, due to the fact that the input space to validate grows exponentially with respect to the number of inputs to validate. Given this limitations, verification techniques based in formal methods arise as an alternative to complement the traditional validation techniques. This dissertation focuses on the application of formal methods to validate the correctness of the partitioned system, with a special focus on the XtratuM hypervisor. The proposed methodology is evaluated through its application to the hypervisor validation. To this end, we propose a formal model of the hypervisor based in Finite State Machines (FSM), this model enables the definition of the correctness properties that the hypervisor design must fulfill. In addition, this dissertation studies how to ensure the functional correctness of the hypervisor implementation by means of deductive code verification techniques. Last, we study the vulnerabilities that result of the loss of confidentiality (CWE-200 [CWE08b]) of the information managed by the partitioned system. In this context, the vulnerabilities (infoleaks) are modeled, static code analysis techniques are applied to the detection of the vulnerabilities, and last the proposed techniques are validated by means of a practical case study on the Linux kernel that is a component of the partitioned system. / [ES] La disponibilidad de nuevos procesadores más potentes para aplicaciones empotradas ha permitido el desarrollo de aplicaciones que abordan problemas de mayor complejidad. Debido a esto, las aplicaciones empotradas actualmente tienen más funciones y prestaciones, y como consecuencia de esto, una mayor complejidad. Por este motivo, existe un interés creciente en permitir la ejecución de múltiples aplicaciones de forma segura y sin interferencias en un mismo procesador y memoria. En este marco surgen las arquitecturas de sistemas particionados basados en hipervisores como una solución apropiada para construir sistemas seguros. Uno de los principales retos en la construcción de sistemas particionados, es la verificación del correcto funcionamiento del hipervisor, dado que es el componente crítico sobre el que descansa la seguridad de todo el sistema particionado. Las técnicas tradicionales de V&V, como testing, inspección y análisis, presentan limitaciones para la verificación exhaustiva del comportamiento del sistema, debido a que el espacio de entradas a verificar crece de forma exponencial con respecto al número de entradas a verificar. Ante estas limitaciones las técnicas de verificación basadas en métodos formales surgen como una alternativa para completar las técnicas de validación tradicional. Esta disertación se centra en la aplicación de métodos formales para validar la corrección del sistema particionado, en especial del hipervisor XtratuM. La validación de la metodología se realiza aplicando las técnicas propuestas a la validación del hipervisor. Para ello, se propone un modelo formal del hipervisor basado en máquinas de autómatas finitos, este modelo formal permite la definición de las propiedades que el diseño hipervisor debe cumplir para asegurar su corrección. Adicionalmente, esta disertación analiza cómo asegurar la corrección funcional de la implementación del hipervisor por medio de técnicas de verificación deductiva de código. Por último, se estudian las vulnerabilidades de tipo information leak (CWE-200 [CWE08b]) debidas a la perdida de la confidencialidad de la información manejada en el sistema particionado. En este ámbito se modelan las vulnerabilidades, se aplican técnicas de análisis de código para la detección de vulnerabilidades en base al modelo definido y por último se valida la técnica propuesta por medio de un caso práctico sobre el núcleo del sistema operativo Linux que forma parte del sistema particionado. / [CAT] La disponibilitat de nous processadors amb major potencia de còmput per a aplicacions empotrades ha permès el desenvolupament de aplicacions que aborden problemes de major complexitat. Degut a açò, les aplicacions empotrades actualment tenen més funcions i prestacions, i com a conseqüència, una major complexitat. Per aquest motiu, existeix un interès creixent en per permetre la execució de múltiples aplicacions de forma segura i sense interferències en un mateix processador i memòria. En aquest marc sorgeixen les arquitectures de sistemes particionats basats en hipervisors com una solució apropiada per a la construcció de sistemes segurs Un dels principals reptes en la construcció de sistemes particionats, es la verificació del correcte funcionament del hipervisor, donat que aquest es el component crític sobre el que descansa la seguretat del sistema particionat complet. Les tècniques tradicionals de V&V, com són el testing, inspecció i anàlisi, presenten limitacions que fan impracticable la seva aplicació per a la verificació exhaustiva del comportament del sistema, degut a que el espai de entrades a verificar creix de forma exponencial amb el nombre de entrades a verificar. Front a aquestes limitacions les tècniques de verificació basades en mètodes formals sorgeixen com una alternativa per a completar les tècniques de validació tradicional. Aquesta dissertació es centra en la aplicació de mètodes formals per a validar la correcció del sistema particionat, en especial d del hipervisor XtratuM. La validació de la metodología es realitza aplicant les tècniques proposades a la validació del hipervisor. Per a aquest fi, es proposa un model formal del hipervisor basat en màquines de estats finits (FSM), aquest model formal permet la definició de les propietats que el disseny del hipervisor deu de complir per assegurar la seva correcció. Addicionalment, aquesta dissertació analitza com assegurar la correcció funcional de la implementació del hipervisor mitjançant tècniques de verificació deductiva de codi. Per últim, s'estudien les vulnerabilitats de tipus information leak (CWE-200 [CWE08b]) degudes a la pèrdua de la confidencialitat de la informació gestionada per el sistema particionat. En aquest àmbit, es modelen les vulnerabilitats, s'apliquen tècniques de anàlisis de codi per a la detecció de les vulnerabilitats en base al model definit, per últim es valida la tècnica proposada mitjançant un cas pràctic sobre el nucli del sistema operatiu Linux que forma part de l'arquitectura particionada. / Peiró Frasquet, S. (2016). Metodología para hipervisores seguros utilizando técnicas de validación formal [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/63152 / TESIS

Motivé par le besoin de la « Conception par Réutilisation », les modèles de processus configurables ont été proposés pour représenter de manière générique des modèles de processus similaires. Ils doivent être configurés en fonction des besoins d’une organisation en sélectionnant des options. Comme les modèles de processus configurables peuvent être larges et complexes, leur configuration sans assistance est sans doute une tâche difficile, longue et source d'erreurs.De plus, les organisations adoptent de plus en plus des environnements Cloud pour déployer et exécuter leurs processus afin de bénéficier de ressources dynamiques à la demande. Néanmoins, en l'absence d'une description explicite et formelle de la perspective de ressources dans les processus métier existants, la correction de la gestion des ressources du Cloud ne peut pas être vérifiée.Dans cette thèse, nous visons à (i) fournir de l’assistance et de l’aide à la configuration aux analystes avec des options correctes, et (ii) améliorer le support de la spécification et de la vérification des ressources Cloud dans les processus métier. Pour ce faire, nous proposons une approche formelle pour aider à la configuration étape par étape en considérant des contraintes structurelles et métier. Nous proposons ensuite une approche comportementale pour la vérification de la configuration tout en réduisant le problème bien connu de l'explosion d'espace d'état. Ce travail permet d'extraire les options de configuration sans blocage d’un seul coup. Enfin, nous proposons une spécification formelle pour le comportement d'allocation des ressources Cloud dans les modèles de processus métier. Cette spécification est utilisée pour valider et vérifier la cohérence de l'allocation des ressources Cloud en fonction des besoins des utilisateurs et des capacités des ressources / Motivated by the need for the “Design by Reuse”, Configurable process models are proposed to represent in a generic manner similar process models. They need to be configured according to an organization needs by selecting design options. As the configurable process models may be large and complex, their configuration with no assistance is undoubtedly a difficult, time-consuming and error-prone task.Moreover, organizations are increasingly adopting cloud environments for deploying and executing their processes to benefit from dynamically scalable resources on demand. Nevertheless, due to the lack of an explicit and formal description of the resource perspective in the existing business processes, the correctness of Cloud resources management cannot be verified.In this thesis, we target to (i) provide guidance and assistance to the analysts in process model configuration with correct options, and to (ii) improve the support of Cloud resource specification and verification in business processes. To do so, we propose a formal approach for assisting the configuration step-by-step with respect to structural and business domain constraints. We thereafter propose a behavioral approach for configuration verification while reducing the well-known state space explosion problem. This work allows to extract configuration choices that satisfy the deadlock-freeness property at one time. Finally, we propose a formal specification for Cloud resource allocation behavior in business process models. This specification is used to formally validate and check the consistency of the Cloud resource allocation in process models according to user requirements and resource capabilities

La contribution principale de cette thèse est un système de preuve correct et complet pour les implications entre les prédicats inductifs, fréquemment rencontrées lors de la vérification des programmes qui utilisent des structures de données récursives allouées dynamiquement. Nous introduisons un système de preuve généralisé pour la logique du premier ordre et nous l'adaptons à la logique de séparation, car ceci est un cadre qui répond aux plusieurs difficultés posées par le raisonnement sur les tas alloués dynamiquement. La correction et la complétude sont assurées par quatre restrictions sémantiques et nous proposons également un semi-algorithme de recherche de preuves qui devient une procédure de décision pour le problème d'implication lorsque les restrictions sémantiques sont respectées.Ce raisonnement d'ordre supérieur sur les implications nécessite des procédures de décision de premier ordre pour la logique sous-jacente lors de l'application des règles d'inférence et lors de la recherche des preuves. Ainsi, nous fournissons deux procédures de décision pour la logique de séparation, en considérant le fragment sans quantificateurs et le fragment quantifié de façon Exists*Forall*, qui ont été intégrées dans le solveur SMT open source CVC4.Finalement, nous présentons une implémentation de notre système de preuve pour la logique de séparation, qui utilise ces procédures de décision. Étant donné des prédicats inductifs et une requête d'implication, un avertissement est émis lorsqu'une ou plusieurs restrictions sémantiques sont violées. Si l'implication est valide, la sortie est une preuve. Sinon, un ou plusieurs contre-exemples sont fournis. / The main contribution of this thesis is a sound and complete proof system for entailments between inductive predicates, which are frequently encountered when verifying programs that work with dynamically allocated recursive data structures. We introduce a generalized proof system for first-order logic, and then adapt it to separation logic, a framework that addresses many of the difficulties posed by reasoning about dynamically allocated heaps. Soundness and completeness are ensured through four semantic restrictions and we also propose a proof-search semi-algorithm that becomes a decision procedure for the entailment problem when the semantic restrictions hold.This higher-order reasoning about entailments requires first-order decision procedures for the underlying logic when applying inference rules and during proof search. Thus, we provide two decision procedures for separation logic, considering the quantifier-free and the Exists*Forall*-quantified fragments, which were integrated in the open-source, DPLL(T)-based SMT solver CVC4.Finally, we also give an implementation of our proof system for separation logic, which uses these decision procedures. Given some inductive predicate definitions and an entailment query as input, a warning is issued when one or more semantic restrictions are violated. If the entailment is found to be valid, the output is a proof. Otherwise, one or more counterexamples are provided.

No description available.

Tato práce popisuje průběh refaktoringu programu mkfs.xfs za účelem zpřehlednění jeho kódu a vyčištění technického dluhu naakumulovaného za dvacet let existence tohoto programu, a následně jeho statickou analýzu. Použité nástroje (CppCheck, Coverity, Codacy, GCC, Clang) jsou srovnány z hlediska počtu i typu nalezených chyb.

The aim of the master's thesis "Analysis of Selected Payment Protocols" is overview of used payment. The first part is concentrated on data security, the second is dedicated to payment protocols, their characteristics, used technology and security elements. The third part is dedicated to verification and simulation tools. Comparison of particular payment protocols and of particular verification tools is part of this work too. Experimental part of the thesis is focused on formalization and verification of the payment protocol Visa 3-D Secure, of the protocol NetBill and on formalization of two subprotocols of SET.