La conception de systèmes embarqués modernes est de plus en plus complexe, car plus de fonctionnalités sont intégrées dans ces systèmes. En même temps, afin de répondre aux exigences de calcul tout en conservant une consommation d'énergie de faible niveau, MPSoCs sont apparus comme les principales solutions pour tels systèmes embarqués. En outre, les systèmes embarqués sont de plus en plus adaptatifs, comme l'adaptabilité peut apporter un certain nombre d'avantages, tels que la flexibilité du logiciel et l'efficacité énergétique. Cette thèse vise la conception sécuritaire de ces MPSoCs adaptatifs. Tout d'abord, chaque configuration de système doit être analysée en ce qui concerne ses propriétés fonctionnelles et non fonctionnelles. Nous présentons un cadre abstraite de conception et d'analyse qui permet des décisions d'implémentation rapide et rentable. Ce cadre est conçu comme un support de raisonnement intermédiaire pour les environnements de co-conception de logiciel / matériel au niveau de système. Il peut élaguer l'espace de conception à sa plus grande portée, et identifier les candidats de solutions de conception de manière rapide et efficace. Dans ce cadre, nous utilisons un codage basé sur l'horloge abstraite pour modéliser les comportements du système. Différents scénarios d'applications de mapping et de planification sur MPSoCs sont analysés via les traces d'horloge qui représentent les simulations du système. Les propriétés d'intérêt sont l'exactitude du comportement fonctionnel, la performance temporelle et la consommation d'énergie. Deuxièmement, la gestion de la reconfiguration de MPSoCs adaptatifs doit être abordée. Nous sommes particulièrement intéressés par les MPSoCs implémentés sur des architectures reconfigurables (ex. FPGAs) qui offrent une bonne flexibilité et une efficacité de calcul pour les MPSoCs adaptatifs. Nous proposons un cadre général de conception basé sur la technique de la synthèse de contrôleurs discrets (DCS) pour résoudre ce problème. L'avantage principal de cette technique est qu'elle permet une synthèse d'un contrôleur automatique selon une spécification des objectifs de contrôle. Dans ce cadre, le comportement de reconfiguration du système est modélisé en termes d'automates synchrones en parallèle. Le problème de calcul de la gestion reconfiguration selon de multiples objectifs concernant, par exemple, les usages des ressources, la performance et la consommation d'énergie, est codé comme un problème de DCS. Le langage de programmation BZR existant et l'outil Sigali sont employés pour effectuer DCS et générer un contrôleur qui satisfait aux exigences du système. Finalement, nous étudions deux façons différentes de combiner les deux cadres de conception proposées pour MPSoCs adaptatifs. Tout d'abord, ils sont combinés pour construire un flot de conception complet pour MPSoCs adaptatifs. Deuxièmement, ils sont combinés pour présenter la façon dont le manager run-time calculé par le second cadre peut être intégré dans le premier cadre afin de réaliser des simulations et des analyses combinées de MPSoCs adaptatifs.

Made available in DSpace on 2014-12-17T15:46:59Z (GMT). No. of bitstreams: 1 BrunoEGG_TESE.pdf: 2215931 bytes, checksum: 5d86c012a04f884e6dec73c92c1d88ef (MD5) Previous issue date: 2012-06-01 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Smart card applications represent a growing market. Usually this kind of application manipulate and store critical information that requires some level of security, such as financial or confidential information. The quality and trustworthiness of smart card software can be improved through a rigorous development process that embraces formal techniques of software engineering. In this work we propose the BSmart method, a specialization of the B formal method dedicated to the development of smart card Java Card applications. The method describes how a Java Card application can be generated from a B refinement process of its formal abstract specification. The development is supported by a set of tools, which automates the generation of some required refinements and the translation to Java Card client (host) and server (applet) applications. With respect to verification, the method development process was formalized and verified in the B method, using the Atelier B tool [Cle12a]. We emphasize that the Java Card application is translated from the last stage of refinement, named implementation. This translation process was specified in ASF+SDF [BKV08], describing the grammar of both languages (SDF) and the code transformations through rewrite rules (ASF). This specification was an important support during the translator development and contributes to the tool documentation. We also emphasize the KitSmart library [Dut06, San12], an essential component of BSmart, containing models of all 93 classes/interfaces of Java Card API 2:2:2, of Java/Java Card data types and machines that can be useful for the specifier, but are not part of the standard Java Card library. In other to validate the method, its tool support and the KitSmart, we developed an electronic passport application following the BSmart method. We believe that the results reached in this work contribute to Java Card development, allowing the generation of complete (client and server components), and less subject to errors, Java Card applications. / As aplica??es para smart cards representam um mercado que cresce a cada ano. Normalmente, essas aplica??es manipulam e armazenam informa??es que requerem garantias de seguran?a, tais como valores monet?rios ou informa??es confidenciais. A qualidade e a seguran?a do software para cart?es inteligentes pode ser aprimorada atrav?s de um processo de desenvolvimento rigoroso que empregue t?cnicas formais da engenharia de software. Neste trabalho propomos o m?todo BSmart, uma especializa??o do m?todo formal B dedicada ao desenvolvimento de aplica??es para smart cards na linguagem Java Card. O m?todo descreve, em um conjunto de etapas, como uma aplica??o smart card pode ser gerada a partir de refinamentos em sua especifica??o formal. O desenvolvimento ? suportado por um conjunto de ferramentas, automatizando a gera??o de parte dos refinamentos e a tradu??o para as aplica??es Java Card cliente (host) e servidora (applet). Ressalta-se que o processo de especifica??o e refinamento descrito no m?todo foi formalizado e verificado utilizando o pr?prio m?todo B, com o aux?lio da ferramenta Atelier B [Cle12a]. Destaca-se que a aplica??o Java Card ? traduzida a partir do ?ltimo passo de refinamento, denominado de implementa??o. A especifica??o dessa tradu??o foi feita na linguagem ASF+SDF [BKV08]. Inicialmente, descreveu-se as gram?ticas das linguagens B e Java (SDF) e, em uma etapa posterior, especificou-se as transforma??es de B para Java Card atrav?s de regras de reescrita de termos (ASF). Essa abordagem foi um importante aux?lio durante o processo de tradu??o, al?m de servir ao prop?sito de document?lo. Cumpre destacar a biblioteca KitSmart [Dut06, San12], componente essencial ao m?todo BSmart, que inclui modelos em B de todas as 93 classes/interfaces da API Java Card na vers?o 2:2:2, dos tipos de dados Java e Java Card e de m?quinas que podem ser ?teis ao especificador, mas que n?o est?o presentes na API padr?o. Tendo em vista validar o m?todo, seu conjunto de ferramentas e a biblioteca KitSmart, procedeu-se com o desenvolvimento, seguindo o m?todo BSmart, de uma aplica??o de passaporte eletr?nico. Os resultados alcan?ados neste trabalho contribuem para o desenvolvimento smart card, na medida em que possibilitam a gera??o de aplica??es Java Card completas (cliente e servidor) e menos sujeitas a falhas.

Information technology systems are essential for most businesses as they facilitate the handling and sharing of data and the execution of tasks. Due to connectivity to the internet and other internal networks, these systems are susceptible to cyberattacks. Computer worms are one of the most significant threats to computer systems because of their fast self-propagation to multiple systems and malicious payloads. Modern worms employ obfuscation techniques to avoid detection using patterns from previous attacks. Although the best defense is to eliminate (patch) the software vulnerabilities being exploited by computer worms, this requires a substantial amount of time to create, test, and deploy the patches. Worm containment techniques are used to reduce or stop the spread of worm infections to allow time for software patches to be developed and deployed. In this dissertation, a novel blockchain-based collaborative intrusion prevention system model is introduced. This model is designed to proactively contain zero-day and obfuscated computer worms. In this model, containment is achieved by creating and distributing signatures for the exploited vulnerabilities. Blockchain technology is employed to provide liveness, maintain an immutable record of vulnerability-based signatures to update peers, accomplish trust in confirming the occurrence of a malicious event and the corresponding signature, and allow a decentralized defensive environment. A consensus algorithm based on the Practical Byzantine Fault Tolerance (PBFT) algorithm is employed in the model. The TLA+ formal method is utilized to check the correctness, liveness, and safety properties of the model as well as to assert that it has no behavioral errors. A blockchain-based automatic worm containment system is implemented. A synthetic worm is created to exploit a network-deployed vulnerable program. This is used to evaluate the effectiveness of the containment system. It is shown that the system can contain the worm and has good performance. The system can contain 100 worm attacks a second by generating and distributing the corresponding vulnerability-based signatures. The system latency to contain these attacks is less than 10 ms. In addition, the system has low resource requirements with respect to memory, CPU, and network traffic. / Graduate

This study examines the specific aspects of the reception of Russian formalism and the development of the Formal method in Soviet Ukrainian culture in the 1920s - the beginning of 1930s. Russian formalism in the process of reception becomes an important tool for the "modernization" of national culture and, as a result, an instrument for a new phase in the construction of national cultural identity. On that basis, the cultural-historical and ideological context of the development of Ukrainian literary criticism, criticism and (partially) literature of the late 19th - first decades of the 20th century is consistently reconstructed in eight chapters of the work. The first chapter highlights theoretical aspects of the study, reviews critical literature, reconstructs the history of reception of Russian formalism in Russian and Western criticism and the history of literature. The second chapter addresses the historical and theoretical premises of the reception of Formal theory in Ukrainian culture. The next chapter discusses historical and political context of the development of literature and literary criticism in 1917-1920 using the example of multinational post-revolutionary Kiev; a brief review of the theoretical and historical works of the 1920s also appears here. A special focus is put on the...

Tendering is a method for entering into a sales contract. Numerous electronic tendering systems have been established with the intent of improving the efficiency of the tendering process. Although providing adequate security services is a desired feature in an e-tendering system, current e-tendering systems are usually designed with little consideration of security and legal compliance. This research focuses on designing secure protocols for e-tendering systems. It involves developing methodologies for establishing security requirements, constructing security protocols and using formal methods in protocol security verification. The implication is that it may prove suitable for developing secure protocols in other electronic business domains. In depth investigations are conducted into a range of issues in relation to establishing generic security requirements for e-tendering systems. The outcomes are presented in a form of basic and advanced security requirements for e-tendering process. This analysis shows that advanced security services are required to secure e-tender negotiation integrity and the submission process. Two generic issues discovered in the course of this research, functional difference and functional limitations, are fundamental in constructing secure protocols for tender negotiation and submission processes. Functional difference identification derives advanced security requirements. Functional limitation assessment defines how the logic of generic security mechanisms should be constructed. These principles form a proactive analysis applied prior to the construction of security protocols. Security protocols have been successfully constructed using generic cryptographic security mechanisms. These protocols are secure e-tender negotiation integrity protocol suite, and secure e-tender submission protocols. Their security has been verified progressively during the design. Verification results show that protocols are secure against common threat scenarios. The primary contribution of this stage are the procedures developed for the complex e-business protocol analysis using formal methods. The research shows that proactive analysis has made this formal security verification possible and practical for complex protocols. These primary outcomes have raised awareness of security issues in e-tendering. The security solutions proposed in the protocol format are the first in e-tendering with verifiable security against common threat scenarios, and which are also practical for implementation. The procedures developed for securing the e-tendering process are generic and can be applied to other business domains. The study has made improvements in: establishing adequate security for a business process; applying proactive analysis prior to secure protocol construction; and verifying security of complex e-business protocols using tool aided formal methods.