Дисертації з теми "Software and hardware protection methods"

Актуальність дослідження. У сучасному світі активно розвиваються мережеві та інформаційні технології. Зараз неможливо в рамках міста знайти будівлю, де б не були розгорнуті підключення до мережі передачі даних на основі технологій Інтернету. Така мережа спрощує і оптимізує велику кількість задач, таких як обмін інформацією, робота над документами, користування програмами, обмін ресурсами та інформацією тощо. В якості такої будівлі доцільно розглянути житловий будинок на визначену кількість квартир. Інформація – це дуже цінний ресурс, тому зловмисники досить часто намагаються отримати доступ до мереж як корпоративних, так і домашніх. Основною причиною впровадження мережевої безпеки є захист мережі та системних ресурсів, підключених до мережі. Інформація в будь-якій формі вважається цінною властивістю мережі, і її втрата чи доступ до неї може коштувати грошей або в гіршому випадку, спричинить катастрофу. Зламування мережі може призвести до різних наслідків: перехоплення даних, зараження шкідливим ПЗ та знищенням усієї інформації. Мета дослідження полягає в пошуку можливостей захисту персональної інформаційної мережі житлового будинку програмно-апаратним комплексом. Завдання для досягнення мети: проаналізувати особливості проектування захищеної персональної інформаційної мережі, зробити огляд мережевої безпеки(можливі вразливості, загрози та атаки), оцінити методи аналізу загроз та відповідно дослідити можливості рішення щодо усування потенційних загроз мережі. Об’єкт дослідження: захищена персональна інформаційна мережа житлового будинку. Предмет дослідження: програмні та програмно апаратні методи захисту персональної інформаційної мережі. Методи дослідження: алгоритми та методи, які визначені в основі функціонування систем та технологій в рамках захищеної локальної мережі, технології та алгоритми методів захисту локальних мереж. Наукова новизна отриманих результатів: 1) запропоновані варіанти створення захищеної персональної інформаційної мережі; 2) запропоновано послідовний алгоритм налаштування програмних методів захисту персональної мережі. Практичне значення одержаних результатів: результати роботи можуть бути використанні при проектуванні домашніх мереж та «будинкових» мереж багатоквартирних будинків.
Relevance of research. In the modern world, network and information technologies are actively developing. At present, it is impossible to find a building within the city where connections to the data network based on Internet technologies have not been deployed. This network simplifies and optimizes many tasks, such as information exchange, working on documents, using programs, exchanging resources and information, and more. As such a building, it is advisable to consider a residential building for a certain number of apartments. Information is a very valuable resource, so attackers often try to access both corporate and home networks. The main reason for implementing network security is to protect the network and system resources connected to the network. Information in any form is considered a valuable property of the network, and its loss or access to it can cost money or, in the worst case, cause a catastrophe. Hacking a network can lead to various consequences: data interception, malware infection and destruction of all information. Therefore, it is important to pay attention to network protection, search for vulnerabilities and identify potential threats that could harm the current system and resources. The purpose of the study is to find opportunities to protect the personal information network of a residential building software and hardware. Objectives to achieve the goal: to analyze the features of designing a secure personal information network, to review network security (possible vulnerabilities, threats and attacks), to evaluate methods of threat analysis and, accordingly, to explore the possibility of solving potential threats to the network. Object of study: protected personal information network of a residential building. Subject of study: software and hardware methods of personal information network protection. Research methods algorithms and methods that are defined in the basis of the functioning of systems and technologies within a secure local area network, technologies and algorithms of local area network protection methods. Scientific novelty of the obtained results: 1) proposed options for creating a secure personal information network; 2) a sequential algorithm for configuring software methods for personal network protection is proposed. The practical implications of the findings: the results of the work can be used in the design of home networks and "home" networks of apartment buildings.

Previously software is distributed to the users by using devices like CD.S and floppies and in the form of bytes. Due to the high usage of internet and in order to perform the tasks rapidly without wasting time on depending physical devices, software is supplied through internet in the form of source code itself. Since source code is available to the end users there is a possibility of changing the source code by malicious users in order to gain their personnel benefits which automatically leads to malfunctioning of the software. The method proposed in this thesis is based on the concept of using hardware to protect the software. We will obfuscate the relation between variables and statements in the software programs so that the attacker can not find the direct relation between them. The method combines software security with code obfuscation techniques, uses the concepts of cryptography like hashing functions and random number generators.

Security of a Multi-Processor System on Chip (MPSoC) is an emerging area of concern in embedded systems. MPSoC security is jeopardized by Code Injection attacks. Code Injection attacks, which are the most common types of software attacks, have plagued single processor systems. Design of MPSoCs must therefore incorporate security as one of the primary objectives. Code Injection attacks exploit vulnerabilities in \trusted" and legacy code. An architecture with a dedicated monitoring processor (MONITOR) is employed to simultaneously supervise the application processors on an MPSoC. The program code in the application processors is divided into basic blocks. The basic blocks in the application processors are statically instrumented with special instructions that allow communication with the MONITOR at runtime. The MONITOR verifies the execution of all the processors at runtime using control flow checks and either a timing or instruction count check. This thesis proposes a monitoring system called SOFTMON, a design methodology called SHIELD, a design flow called LOCS and an architectural framework called CUFFS for detecting Code Injection attacks. SOFTMON, a software monitoring system, uses a software algorithm in the MONITOR. SOFTMON incurs limited area overheads. However, the runtime performance overhead is quite high. SHIELD, an extension to the work in SOFTMON overcomes the limitation of high runtime overhead using a MONITOR that is predominantly hardware based. LOCS uses only one special instruction per basic block compared to two, as was the case in SOFTMON and SHIELD. Additionally, profile information is generated for all the basic blocks in all the application processors for the MPSoC designer to tune the design by increasing or decreasing the frequency of loop basic blocks. CUFFS detects attacks even without application processors communicating to the MONITOR. The SOFTMON, SHIELD and LOCS approaches can only detect attacks if the application processors communicate to the MONITOR. CUFFS relies on the exact number of instructions in basic blocks to determine an attack, rather than time-frame based measures used in SOFTMON, SHIELD and LOCS. The lowest runtime performance overhead was achieved by LOCS (worst case of 37.5%), while the SOFTMON monitoring system had the least amount of area overheads of about 25%. The CUFFS approach employed an active MONITOR and hence detected a greater range of attacks. The CUFFS framework also detects bit flip errors (reliability errors) in the control flow instructions of the application processors on an MPSoC. CUFFS can detect nearly 70% of all bit flip errors in the control flow instructions. Additionally, a modified CUFFS approach is proposed to ensure reliable inter-processor communication on an MPSoC. The modified CUFFS approach uses a hardware based checksum approach for reliable inter-processor communication and incurred a runtime performance overhead of up to 25% and negligible area overheads compared to CUFFS. Thus, the approaches proposed in this thesis equip an MPSoC designer with tools to embed security features during an MPSoC's design phase. Incorporating security measures at the processor design level provides security against software attacks in MPSoCs and incurs manageable runtime, area and code-size overheads.

Analog technology has been around for a long time. The use of analog technology is necessary since we live in an analog world. However, the transmission and storage of analog technology is more complicated and in many cases less efficient than digital technology. Digital technology, on the other hand, provides fast means to be transmitted and stored. Digital technology continues to grow and it is more widely used than ever before. However, with the advent of new technology that can reproduce digital documents or images with unprecedented accuracy, it poses a risk to the intellectual rights of many artists and also on personal security. One way to protect intellectual rights of digital works is by embedding watermarks in them. The watermarks can be visible or invisible depending on the application and the final objective of the intellectual work. This thesis deals with watermarking images in the discrete wavelet transform domain. The watermarking process was done using the JPEG2000 compression standard as a platform. The hardware implementation was achieved using the ALTERA DSP Builder and SIMULINK software to program the DE2 ALTERA FPGA board. The JPEG2000 color transform and the wavelet transformation blocks were implemented using the hardware-in-the-loop (HIL) configuration.

Hardware/Software (HW/SW) interfaces are pervasive in modern computer systems. Most of HW/SW interfaces are implemented by devices and their device drivers. Unfortunately, HW/SW interfaces are unreliable and insecure due to their intrinsic complexity and error-prone nature. Moreover, assuring HW/SW interface reliability and security is challenging. First, at the post-silicon validation stage, HW/SW integration validation is largely an ad-hoc and time-consuming process. Second, at the system deployment stage, transient hardware failures and malicious attacks make HW/SW interfaces vulnerable even after intensive testing and validation. In this dissertation, we present a comprehensive solution for HW/SW interface assurance over the system life cycle. This solution is composited of two major parts. First, our solution provides a systematic HW/SW co-validation framework which validates hardware and software together; Second, based on the co-validation framework, we design two schemes for assuring HW/SW interfaces over the system life cycle: (1) post-silicon HW/SW co-validation at the post-silicon validation stage; (2) HW/SW co-monitoring at the system deployment stage. Our HW/SW co-validation framework employs a key technique, conformance checking which checks the interface conformance between the device and its reference model. Furthermore, property checking is carried out to verify system properties over the interactions between the reference model and the driver. Based on the conformance between the reference model and the device, properties hold on the reference model/driver interface also hold on the device/driver interface. Conformance checking discovers inconsistencies between the device and its reference model thereby validating device interface implementations of both sides. Property checking detects both device and driver violations of HW/SW interface protocols. By detecting device and driver errors, our co-validation approach provides a systematic and ecient way to validate HW/SW interfaces. We developed two software tools which implement the two assurance schemes: DCC (Device Conformance Checker), a co-validation framework for post-silicon HW/SW integration validation; and CoMon (HW/SW Co-monitoring), a runtime verication framework for detecting bugs and malicious attacks across HW/SW interfaces. The two software tools lead to discovery of 42 bugs from four industry hardware devices, the device drivers, and their reference models. The results have demonstrated the signicance of our approach in HW/SW interface assurance of industry applications.

While microprocessors have doubled their speed every 18 months, performance improvement of memory systems has continued to lag behind. to address the speed gap between CPU and memory, a standard multi-level caching organization has been built for fast data accesses before the data have to be accessed in DRAM core. The existence of these caches in a computer system, such as L1, L2, L3, and DRAM row buffers, does not mean that data locality will be automatically exploited. The effective use of the memory hierarchy mainly depends on how data are allocated and how memory accesses are scheduled. In this dissertation, we propose several novel software and hardware techniques to effectively exploit the data locality and to significantly reduce memory access latency.;We first presented a case study at the application level that reconstructs memory-intensive programs by utilizing program-specific knowledge. The problem of bit-reversals, a set of data reordering operations extensively used in scientific computing program such as FFT, and an application with a special data access pattern that can cause severe cache conflicts, is identified in this study. We have proposed several software methods, including padding and blocking, to restructure the program to reduce those conflicts. Our methods outperform existing ones on both uniprocessor and multiprocessor systems.;The access latency to DRAM core has become increasingly long relative to CPU speed, causing memory accesses to be an execution bottleneck. In order to reduce the frequency of DRAM core accesses to effectively shorten the overall memory access latency, we have conducted three studies at this level of memory hierarchy. First, motivated by our evaluation of DRAM row buffer's performance roles and our findings of the reasons of its access conflicts, we propose a simple and effective memory interleaving scheme to reduce or even eliminate row buffer conflicts. Second, we propose a fine-grain priority scheduling scheme to reorder the sequence of data accesses on multi-channel memory systems, effectively exploiting the available bus bandwidth and access concurrency. In the final part of the dissertation, we first evaluate the design of cached DRAM and its organization alternatives associated with ILP processors. We then propose a new memory hierarchy integration that uses cached DRAM to construct a very large off-chip cache. We show that this structure outperforms a standard memory system with an off-level L3 cache for memory-intensive applications.;Memory access latency has become a major performance bottleneck for memory-intensive applications. as long as DRAM technology remains its most cost-effective position for making main memory, the memory performance problem will continue to exist. The studies conducted in this dissertation attempt to address this important issue. Our proposed software and hardware schemes are effective and applicable, which can be directly used in real-world memory system designs and implementations. Our studies also provide guidance for application programmers to understand memory performance implications, and for system architects to optimize memory hierarchies.

L'injection de faute est une méthode bien connue pour évaluer la robustesse et détecter les vulnérabilités des systèmes. La détection des vulnérabilités créées par injection de fautes a été approchée par différentes méthodes. Dans la littérature deux approches existent: les approches logicielles et les approches matérielles. Les approches logicielles peuvent fournir une large et rapide couverture, mais ne garantissent pas la présence de vulnérabilité dans le système. Les approches matérielles sont incontestables dans leurs résultats, mais nécessitent l’utilisation de matériaux assez coûteux et un savoir-faire approfondi, qui ne permet tout de même pas dans la majorité des cas de confirmer le modèle de faute représentant l'effet créé. Dans un premier lieu, cette thèse se concentre sur l'approche logicielle et propose une approche automatisée qui emploie les techniques de la vérification formelle pour détecter des vulnérabilités créées par injection de faute au niveau binaire. L'efficacité de cette approche est montrée en l'appliquant à des algorithmes de cryptographie implémentés dans les systèmes embarqués. Dans un second lieu, cette thèse établit un rapprochement entre les deux approches logicielles et matérielles sur la détection de vulnérabilité d'injection de faute en comparant les résultats des expériences des deux approches. Ce rapprochement des deux approches démontre que: toutes les vulnérabilités détectées par l'approche logicielle ne peuvent pas être reproduites dans le matériel; les conjectures antérieures sur le modèle de faute par des attaques d'impulsion électromagnétique ne sont pas précises ; et qu’il y a un lien entre les résultats de l’approche logicielle et l'approche matérielle. De plus, la combinaison des deux approches peut rapporter une approche plus précise et plus efficace pour détecter les vulnérabilités qui peuvent être créées par injection de faute
Fault injection is a well known method to test the robustness and security vulnerabilities of systems. Detecting fault injection vulnerabilities has been approached with a variety of different but limited methods. Software-based and hardware-based approaches have both been used to detect fault injection vulnerabilities. Software-based approaches can provide broad and rapid coverage, but may not correlate with genuine hardware vulnerabilities. Hardware-based approaches are indisputable in their results, but rely upon expensive expert knowledge, manual testing, and can not confirm what fault model represent the created effect. First, this thesis focuses on the software-based approach and proposes a general process that uses model checking to detect fault injection vulnerabilities in binaries. The efficacy and scalability of this process is demonstrated by detecting vulnerabilities in different cryptographic real-world implementations. Then, this thesis bridges software-based and hardware-based fault injection vulnerability detection by contrasting results of the two approaches. This demonstrates that: not all software-based vulnerabilities can be reproduced in hardware; prior conjectures on the fault model for electromagnetic pulse attacks may not be accurate; and that there is a relationship between software-based and hardware-based approaches. Further, combining both software-based and hardware-based approaches can yield a vastly more accurate and efficient approach to detect genuine fault injection vulnerabilities

JPEG2000 is a wavelet transform based image compression and coding standard. It provides superior rate-distortion performance when compared to the previous JPEG standard. In addition JPEG2000 provides four dimensions of scalability-distortion, resolution, spatial, and color. These superior features make JPEG2000 ideal for use in power and bandwidth limited mobile applications like urban search and rescue. Such applications require a fast, low power JPEG2000 encoder to be embedded on the mobile agent. This embedded encoder needs to also provide superior subjective quality to low bitrate images. This research addresses these two aspects of enhancing the performance of JPEG2000 encoders. The JPEG2000 standard includes a perceptual weighting method based on the contrast sensitivity function (CSF). Recent literature shows that perceptual methods based on subband standard deviation are also effective in image compression. This research presents two new perceptual weighting methods that combine information from both the human contrast sensitivity function as well as the standard deviation within a subband or code-block. These two new sets of perceptual weights are compared to the JPEG2000 CSF weights. The results indicate that our new weights performed better than the JPEG2000 CSF weights for high frequency images. Weights based solely on subband standard deviation are shown to perform worse than JPEG2000 CSF weights for all images at all compression ratios. Embedded block coding, EBCOT tier-1, is the most computationally intensive part of the JPEG2000 image coding standard. Past research on fast EBCOT tier-1 hardware implementations has concentrated on cycle efficient context formation. These pass-parallel architectures require that JPEG2000's three mode switches be turned on. While turning on the mode switches allows for arithmetic encoding from each coding pass to run independent of each other (and thus in parallel), it also disrupts the probability estimation engine of the arithmetic encoder, thus sacrificing coding efficiency for improved throughput. In this research a new fast EBCOT tier-1 design is presented: it is called the Split Arithmetic Encoder (SAE) process. The proposed process exploits concurrency to obtain improved throughput while preserving coding efficiency. The SAE process is evaluated using three methods: clock cycle estimation, multithreaded software implementation, a field programmable gate array (FPGA) hardware implementation. All three methods achieve throughput improvement; the hardware implementation exhibits the largest speedup, as expected. A high speed, task-parallel, multithreaded, software architecture for EBCOT tier-1 based on the SAE process is proposed. SAE was implemented in software on two shared-memory architectures: a PC using hyperthreading and a multi-processor non-uniform memory access (NUMA) machine. The implementation adopts appropriate synchronization mechanisms that preserve the algorithm's causality constraints. Tests show that the new architecture is capable of improving throughput as much as 50% on the NUMA machine and as much as 19% on a PC with two virtual processing units. A high speed, multirate, FPGA implementation of the SAE process is also proposed. The mismatch between the rate of production of data by the context formation (CF) module and the rate of consumption of data by the arithmetic encoder (AE) module is studied in detail. Appropriate choices for FIFO sizes and FIFO write and read capabilities are made based on the statistics obtained from test runs of the algorithm. Using a fast CF module, this implementation was able to achieve as much as 120% improvement in throughput.
Ph. D.

Dans ces travaux de thèse, nous nous intéressons à une classe de stratégies d'application de politiques de sécurité que nous appelons HSE, pour Hardware-based Security Enforcement. Dans ce contexte, un ou plusieurs composants logiciels de confiance contraignent l'exécution du reste de la pile logicielle avec le concours de la plate-forme matérielle sous-jacente afin d'assurer le respect d'une politique de sécurité donnée. Pour qu'un mécanisme HSE contraigne effectivement l'exécution de logiciels arbitraires, il est nécessaire que la plate-forme matérielle et les composants logiciels de confiance l'implémentent correctement.Ces dernières années, plusieurs vulnérabilités ont mis à défaut des implémentations de mécanismes HSE. Nous concentrons ici nos efforts sur celles qui sont le résultat d'erreurs dans les spécifications matérielles et non dans une implémentation donnée.Plus précisément, nous nous intéressons aux cas particulier de l'usage légitime, par un attaquant, d'une fonctionnalité d'un composant matériel pour contourner les protections offertes par un second. Notre but est d'explorer des approches basées sur l'usage de méthodes formelles pour spécifier et vérifier des mécanismes HSE. La spécification de mécanismes HSE peut servir de point de départ pour la vérification des spécifications matérielles concernées, dans l'espoir de prévenir des attaques profitant de la composition d'un grand nombre de composants matériels. Elles peuvent ensuite être fournies aux développeurs logiciels, sous la forme d'une liste de prérequis que leurs produits doivent respecter s'ils désirent l'application d'une politique de sécurité clairement identifiée
In this thesis, we consider a class of security enforcement mechanisms we called Hardware-based Security Enforcement (HSE). In such mechanisms, some trusted software components rely on the underlying hardware architecture to constrain the execution of untrusted software components with respect to targeted security policies. For instance, an operating system which configures page tables to isolate userland applications implements a HSE mechanism. For a HSE mechanism to correctly enforce a targeted security policy, it requires both hardware and trusted software components to play their parts. During the past decades, several vulnerability disclosures have defeated HSE mechanisms. We focus on the vulnerabilities that are the result of errors at the specification level, rather than implementation errors. In some critical vulnerabilities, the attacker makes a legitimate use of one hardware component to circumvent the HSE mechanism provided by another one. For instance, cache poisoning attacks leverage inconsistencies between cache and DRAM’s access control mechanisms. We call this class of attacks, where an attacker leverages inconsistencies in hardware specifications, compositional attacks. Our goal is to explore approaches to specify and verify HSE mechanisms using formal methods that would benefit both hardware designers and software developers. Firstly, a formal specification of HSE mechanisms can be leveraged as a foundation for a systematic approach to verify hardware specifications, in the hope of uncovering potential compositional attacks ahead of time. Secondly, it provides unambiguous specifications to software developers, in the form of a list of requirements

A popularização dos dispositivos móveis impulsionou a pesquisa e o desenvolvimento de soluções de baixo consumo. A evolução destas aplicações demanda ferramentas que permitam avaliar diferentes alternativas de implementação, fornecendo, aos desenvolvedores, informações valiosas para a criação de soluções energeticamente eficientes. Este trabalho desenvolveu uma nova plataforma de medição de consumo que permite comparar a eficiência energética de diferentes algoritmos implementados em software e em hardware. A plataforma é capaz de medir o consumo energético de um processo específico em execução em um processador de propósito geral com um sistema operacional padrão, além de comparar o resultado obtido com algoritmos equivalentes implementados em uma FPGA. Isto permite ao desenvolvedor dividir o processamento da aplicação entre software e hardware de forma a obter a solução mais energeticamente eficiente. Comparada com o estado da arte, a plataforma de medição criada possui três característica inovadoras: suporte a medição de consumo de software e hardware; medição de trechos de código específicos executados pelo processador; e suporte a alteração dinâmica do clock. Também é mostrado neste trabalho como a plataforma desenvolvida tem sido utilizada para analisar o consumo energético de algoritmos de detecção de intrusão de rede para ataques do tipo probing.
The large number of mobile devices increased the interest in low-power designs. Tools that allow the evaluation of alternative implementations give the designer actionable information to create energy-efficient designs. This paper presents a new power measurement platform able to compare the energy consumption of different algorithms implemented in software and in hardware. The proposed platform is able to measure the energy consumption of a specific process running in a general-purpose CPU with a standard operating system, and to compare the results with equivalent algorithms running in an FPGA. This allows the designer to choose the most energy-efficient software vs. hardware partitioning for a given application. Compared with the current state-of-the-art, the presented platform has four distinguishing features: (i) support for both software and hardware power measurements, (ii) measurement of individual code sections in the CPU, (iii) support for dynamic clock frequencies, and (iv) improvement of measurement precision. We also demonstrate how the developed platform has been used to analyze the energy consumption of network intrusion detection algorithms aimed at detecting probing attacks.

Security of cryptographic algorithms relies on the computational difficulty of deriving the secret key using public information. Cryptanalysis, including logical and implementation attacks, plays an important role in allowing the security community to estimate their cost, based on the computational resources of an attacker. Practical implementations of cryptanalytic systems require complex designs that integrate multiple functional components with many parameters. In this thesis, methodologies are proposed to improve the design process of cryptanalytic systems and reduce the cost of design space exploration required for optimization. First, Bluespec, a rule-based HDL, is used to increase the abstraction level of hardware design and support efficient design space exploration. Bluespec is applied to implement a hardware-accelerated logical attack on ECC with optimized modular arithmetic components. The language features of Bluespec support exploration and this is demonstrated by applying Bluespec to investigate the speed area tradeoff resulting from various design parameters and demonstrating performance that is competitive with prior work. This work also proposes a testing environment for use in verifying the implementation attack resistance of secure systems. A modular design approach is used to provide separation between the device being tested and the test script, as well as portability, and openness. This yields an open-source solution that supports implementation attack testing independent of the system platform, implementation details, and type of attack under evaluation. The suitability of the proposed test environment for implementation attack vulnerability analysis is demonstrated by applying the environment to perform an implementation attack on AES. The design of complex cryptanalytic hardware can greatly benefit from better design methodologies and the results presented in this thesis advocate the importance of this aspect.
Master of Science

En considérant la vitesse avec laquelle la technologie des systèmes embarqués progresse, il n’est pas étonnant que le nombre des attaques des systèmes soit en nette augmentation. De nombreuses applications sont développées rapidement et sont écrites avec un langage bas niveau pour suivre le rythme avec lequel progresse l’industrie des systèmes embarqués. Souvent, ces applications contiennent beaucoup de bugs. Certains bugs peuvent être exploités pour pénétrer un système et exécuter un code malveillant. Aujourd’hui, la revue de code peut s’avérer très coûteuse vu la taille des codes développés. En outre, une revue détaillée de code ne garantit pas un système infaillible.Cette thèse présente une architecture permettant l'exécution de plusieurs applications sécurisées et non sécurisées sur une même plate-forme « légère ». Notre architecture doit garantir que même s’il y a une application compromise, les attaquants ne peuvent pas compromettre la totalité du système et/ou récupérer les données des autres applications. Elle doit garantir une forte séparation entre tous les périphériques et les applications présents sur la plate-forme. Finalement, elle doit aussi être capable de vérifier l’état de n’importe quel bout de code. Pour pouvoir garantir ces points, nous utiliserons des techniques d’isolation et d’attestation.Dans un premier temps, nous avons étudié plusieurs architectures d’isolation et d’attestation décrites dans la littérature et utilisés par l’industrie. L’étude a montré qu’il existe une grande variété d’architectures intéressantes offrant différents niveaux de protection et visant différents systèmes. Les systèmes avec une grande capacité de calcul proposent un bon niveau de protection. Par contre, les systèmes « légers », qui ont des ressources très limitées et doivent répondre aux contraintes temporelles, échouent dans au moins un des critères suivants : l’isolation, les performances, le coût, ou bien la flexibilité.À l’issue de cette étude, nous avons conçu Toubkal. Une solution hybride (Co-design logiciel et matériel) pour offrir une architecture d’isolation et d’attestation modulaire qui permet d’établir une isolation sur plusieurs niveaux, de détecter la présence d’un logiciel malveillant ou une donnée malveillante avec des performances acceptables et un coût réduit.Toubkal est principalement composé de trois modules ; deux matériels et un logiciel. Le premier module, appelé Master Memory Protection, permet de créer un premier niveau d’isolation pour contrôler les accès mémoire des périphériques. Le deuxième module, appelé Execution Aware Protection, permet de renforcer la protection d’un logiciel critique, y compris le système d’exploitation. Ces deux niveaux d’isolation permettent de réduire la surface d’attaque.L’isolation toute seule ne suffit pas pour garantir que les applications fonctionnent comme il le faut. En fait, l’attaquant peut toujours modifier le comportement d’une application faillible. Pour cela, Toubkal propose un root immuable qui permet d’attester l’intégrité des autres applications.Pour valider le design de Toubkal, nous avons défini des propriétés de sécurité que nous avons prouvé avec la vérification formelle. Nous avons aussi évalué la taille de Toubkal. Les résultats montrent que le coût de Toubkal est acceptable pour un système dit « léger ».Finalement, nous avons conclu cette thèse avec une discussion des limitations de Toubkal et les perspectives pour améliorer le design et offrir plus de protection, comme par exemple le chiffrement du code à coût caché
Looking at the speed by which embedded systems technologies are advancing, there is no surprise the attacks' number is rising. Many applications are written quickly in a low-level language to keep up with industry pace, and they contain a variety of bugs. Bugs can be used to break into a device and to run malicious code. Reviewing code becomes more and more complex and costly due to its size. Another factor complicating code review is the use of on-the-shelf libraries. Even a detailed code review does not guarantee a bug-free application.This thesis presents an architecture to run securely untrusted applications on the same platform. We assume that the applications contain exploitable bugs, even the operating system can be exploited. We also assume that attackers can take control of In/Out hardware components (e.g., Direct Memory Access (DMA)). The device is trusted when the architecture guarantees that attackers cannot compromise the whole device and access sensitive code and data. Even when an application is compromised, our architecture guarantees a strong separation of multiple components: hardware and software. It ensures the authenticity and integrity of embedded applications and can verify their state before any sensitive operation. The architecture guarantees, for local and remote parties, that the device is running properly, and protect against software attacks.First, we study multiple attack vector and isolation and attestation architectures. We present multiple software attack vectors, and we define the security features and properties that these architectures need to ensure. We provide a detailed description of fifteen existing architectures in both academia and industry, and we compare their features. Then, we provide an in-depth study of five lightweight architectures where we give a comparison of performance, size, and how they behave against software-based attacks. From these studies, we draw our security objectives for lightweight devices: multi-layer isolation, attestation, upgradability, confidentiality, small size with a negligible run-time overhead and ease-of-use.Then, we design hybrid isolation and attestation architecture for lightweight devices. The so-called Toubkal offers multi-layered isolation; the system is composed of three layers of isolation. The first one is at the hardware level to separate In/Out components from each other. The second one is at the security monitor level; our study shows that there is a strong need to create a real separation between the security monitor and all the rest. Finally, the third layer is at the application level.However, isolation itself is not sufficient. Devices still need to ensure that the running application behaves as it was intended. For this reason, Toubkal provides attestation to be able to check the state of a device at any-time. It guarantees that a software component or data were not compromised.Finally, we prove the correctness of the security properties that Toubkal provides. We modeled Toubkal as a finite state machine and used computer-aided formal verification to prove the security properties. Then, we evaluated Toubkal's overhead. The results show that Toubkal overhead is small and fit for lightweight devices

O câncer é responsável por cerca de 7 milhões de óbitos anuais em todo o mundo. Estima-se que 25% de todos os cânceres são de pele, sendo no Brasil o tipo mais incidente em todas as regiões geográficas. Entre eles, o tipo melanoma, responsável por 4% dos cânceres de pele, cuja incidência dobrou mundialmente nos últimos dez anos. Entre os métodos diagnósticos empregados, cita-se a regra ABCD, que leva em consideração assimetria (A), bordas (B), cor (C) e diâmetro (D) de manchas ou nevos. O processamento digital de imagens tem mostrado um bom potencial para auxiliar no diagnóstico precoce de melanomas. Neste sentido, o objetivo do presente estudo foi desenvolver um software, na plataforma MATLAB®, associado a um hardware para padronizar a aquisição de imagens, visando realizar o diagnóstico e acompanhamento de lesões cutâneas suspeitas de malignidade (melanoma). Utilizou-se como norteador a regra ABCD para o desenvolvimento de métodos de análise computacional. Empregou-se o MATLAB como ambiente de programação para o desenvolvimento de um software para o processamento digital de imagens. As imagens utilizadas foram adquiridas de dois bancos de imagens de acesso livre. Foram inclusas imagens de melanomas (n=15) e imagens nevos (não câncer) (n=15). Utilizaram-se imagens no canal de cor RGB, as quais foram convertidas para escala de cinza, aplicação de filtro de mediana 8x8 e técnica de aproximação por vizinhança 3x3. Após, procedeu-se a binarização e inversão de preto e branco para posterior extração das características do contorno da lesão. Para a aquisição padronizada de imagens foi desenvolvido um protótipo de hardware, o qual não foi empregado neste estudo (que utilizou imagens com diagnóstico fechado, de bancos de imagem), mas foi validado para a avaliação do diâmetro das lesões (D). Utilizou-se a estatística descritiva onde os grupos foram submetidos ao teste não paramétrico para duas amostras independentes de Mann-Whitney U. Ainda, para avaliar a sensibilidade (SE) e especificidade (SP) de cada variável, empregou-se a curva ROC. O classificador utilizado foi uma rede neural artificial de base radial, obtendo acerto diagnóstico para as imagens melanomas de 100% e para imagens não câncer de 90,9%. Desta forma, o acerto global para predição diagnóstica foi de 95,5%. Em relação a SE e SP do método proposto, obteve uma área sob a curva ROC de 0,967, o que sugere uma excelente capacidade de predição diagnóstica, sobretudo, com baixo custo de utilização, visto que o software pode ser executado na grande maioria dos sistemas operacionais hoje utilizados.
Cancer is responsible for about 7 million deaths annually worldwide. It is estimated that 25% of all cancers are skin, and in Brazil the most frequent in all geographic regions type. Among them, the melanoma type, accounting for 4% of skin cancers, whose incidence has doubled worldwide in the past decade. Among the diagnostic methods employed, it is cited ABCD rule which considers asymmetry (A), edges (B), color (C) and diameter (D) stains or nevi. The digital image processing has shown good potential to aid in early diagnosis of melanoma. In this sense, the objective of this study was to develop software in MATLAB® platform, associated with hardware to standardize image acquisition aiming at performing the diagnosis and monitoring of suspected malignancy (melanoma) skin lesions. Was used as the ABCD rule for guiding the development of methods of computational analysis. We used MATLAB as a programming environment for the development of software for digital image processing. The images used were acquired two banks pictures free access. Images of melanomas (n = 15) and pictures nevi (not cancer) (n = 15) were included. We used the image in RGB color channel, which were converted to grayscale, application of 8x8 median filter and approximation technique for 3x3 neighborhood. After we preceded binarization and reversing black and white for subsequent feature extraction contours of the lesion. For the standardized image acquisition was developed a prototype hardware, which was not used in this study (that used with enclosed diagnostic images of image banks), but has been validated for evaluation of lesion diameter (D). We used descriptive statistics where the groups were subjected to non-parametric test for two independent samples Mann-Whitney U test yet, to evaluate the sensitivity (SE) and specificity (SP) of each variable, we used the ROC curve. The classifier used was an artificial neural network with radial basis function, obtaining diagnostic accuracy for melanoma images and 100% for images not cancer of 90.9%. Thus, the overall diagnostic accuracy for prediction was 95.5%. Regarding the SE and SP of the proposed method, obtained an area under the ROC curve of 0.967, which suggests an excellent diagnostic ability to predict, especially with low costs, since the software can be run in most systems operational use today.

The complexity of the software behind autonomous systems is rapidly growing, as are the applications of what they can do. It is not unusual for the lines of code to reach the millions, which adds to the verification challenge. The machine learning algorithms involved are often "black boxes" where the precise workings are not known by the developer applying them, and their behavior is undefined when encountering an untrained scenario. With so much code, the possibility of bugs or malicious code is considerable. An approach is developed to monitor and possibly override the behavior of autonomous systems independent of the software controlling them. Application-isolated safety monitors are implemented in configurable hardware to ensure that the behavior of an autonomous system is limited to what is intended. The sensor inputs may be shared with the software, but the output from the monitors is only engaged when the system violates its prescribed behavior. For each specific rule the system is expected to follow, a monitor is present processing the relevant sensor information. The behavior is defined in linear temporal logic (LTL) and the associated monitors are implemented in a field programmable gate array (FPGA). An off-the-shelf drone is used to demonstrate the effectiveness of the monitors without any physical modifications to the drone. Upon detection of a violation, appropriate corrective actions are persistently enforced on the autonomous system.
Master of Science
Autonomous systems are surprisingly vulnerable, not just from malicious hackers, but from design errors and oversights. The lines of code required can quickly climb into the millions, and the artificial decision algorithms can be inscrutable and fully dependent upon the information they are trained on. These factors cause the verification of the core software running our autonomous cars, drones, and everything else to be prohibitively difficult by traditional means. Independent safety monitors are implemented to provide internal oversight for these autonomous systems. A semi-automatic design process efficiently creates error-free monitors from safety rules drones need to follow. These monitors remain separate and isolated from the software typically controlling the system, but use the same sensor information. They are embedded in the circuitry and act as their own small, task-specific processors watching to make sure a particular rule is not violated; otherwise, they take control of the system and force corrective behavior. The monitors are added to a consumer off-the-shelf (COTS) drone to demonstrate their effectiveness. For every rule monitored, an override is triggered when they are violated. Their effectiveness depends on reliable sensor information as with any electronic component, and the completeness of the rules detailing these monitors.

CAPES; CNPq
O constante aumento na velocidade da rede, o número de ataques e a necessidade de eficiência energética estão fazendo com que a segurança de rede baseada em software chegue ao seu limite. Um tipo comum de ameaça são os ataques do tipo probing, nos quais um atacante procura vulnerabilidades a partir do envio de pacotes de sondagem a uma máquina-alvo. Este trabalho apresenta o estudo, o desenvolvimento e a implementação de um algoritmo de extração de características dos pacotes da rede em hardware e de três classificadores de aprendizagem de máquina (Árvore de Decisão, Naive Bayes e k-vizinhos mais próximos), em software e hardware, para a detecção de ataques do tipo probing. O trabalho apresenta, ainda resultados detalhados de acurácia de classificação, taxa de transferência e consumo de energia para cada implementação.
The increasing network speeds, number of attacks, and need for energy efficiency are pushing software-based network security to its limits. A common kind of threat is probing attacks, in which an attacker tries to find vulnerabilities by sending a series of probe packets to a target machine. This work presents the study, development, and implementation of a network packets feature extraction algorithm in hardware and three machine learning classifiers (Decision Tree, Naive Bayes, and k-nearest neighbors), in software and hardware, for the detection of probing attacks. The work also presents detailed results of classification accuracy, throughput, and energy consumption for each implementation.

The aim of the work was design and realization of device to simplify and speed up the testing of AWS / TPWS train protection system. The first chapter is addressed to description and division of train protection systems. The next chapter describes the process of commissioning the AWS / TPWS system and possible applycation of the device to this process. The final chapters deal with design, specification of components, realization of device and verification of its functionality.

Le respect de la vie privée par construction est de plus en plus mentionné comme une étape essentielle vers une meilleure protection de la vie privée. Les nouvelles technologies de l'information et de la communication donnent naissance à de nouveaux modèles d'affaires et de services. Ces services reposent souvent sur l'exploitation de données personnelles à des fins de personnalisation. Alors que les exigences de respect de la vie privée sont de plus en plus sous tension, il apparaît que les technologies elles-mêmes devraient être utilisées pour proposer des solutions davantage satisfaisantes. Les technologies améliorant le respect de la vie privée ont fait l'objet de recherches approfondies et diverses techniques ont été développées telles que des anonymiseurs ou des mécanismes de chiffrement évolués. Cependant, le respect de la vie privée par construction va plus loin que les technologies améliorant simplement son respect. En effet, les exigences en terme de protection des données à caractère personnel doivent être prises en compte au plus tôt lors du développement d’un système car elles peuvent avoir un impact important sur l'ensemble de l'architecture de la solution. Cette approche peut donc être résumée comme « prévenir plutôt que guérir ». Des principes généraux ont été proposés pour définir des critères réglementaires de respect de la vie privée. Ils impliquent des notions telles que la minimisation des données, le contrôle par le sujet des données personnelles, la transparence des traitements ou encore la redevabilité. Ces principes ne sont cependant pas suffisamment précis pour être directement traduits en fonctionnalités techniques. De plus, aucune méthode n’a été proposée jusqu’ici pour aider à la conception et à la vérification de systèmes respectueux de la vie privée. Cette thèse propose une démarche de spécification, de conception et de vérification au niveau architectural. Cette démarche aide les concepteurs à explorer l'espace de conception d'un système de manière systématique. Elle est complétée par un cadre formel prenant en compte les exigences de confidentialité et d’intégrité des données. Enfin, un outil d’aide à la conception permet aux concepteurs non-experts de vérifier formellement les architectures. Une étude de cas illustre l’ensemble de la démarche et montre comment ces différentes contributions se complètent pour être utilisées en pratique
Privacy by Design (PbD) is increasingly praised as a key approach to improving privacy protection. New information and communication technologies give rise to new business models and services. These services often rely on the exploitation of personal data for the purpose of customization. While privacy is more and more at risk, the growing view is that technologies themselves should be used to propose more privacy-friendly solutions. Privacy Enhancing Technologies (PETs) have been extensively studied, and many techniques have been proposed such as anonymizers or encryption mechanisms. However, PbD goes beyond the use of PETs. Indeed, the privacy requirements of a system should be taken into account from the early stages of the design because they can have a large impact on the overall architecture of the solution. The PbD approach can be summed up as ``prevent rather than cure''. A number of principles related to the protection of personal data and privacy have been enshrined in law and soft regulations. They involve notions such as data minimization, control of personal data by the subject, transparency of the data processing, or accountability. However, it is not clear how to translate these principles into technical features, and no method exists so far to support the design and verification of privacy compliant systems. This thesis proposes a systematic process to specify, design, and verify system architectures. This process helps designers to explore the design space in a systematic way. It is complemented by a formal framework in which confidentiality and integrity requirements can be expressed. Finally, a computer-aided engineering tool enables non-expert designers to perform formal verifications of the architectures. A case study illustrates the whole approach showing how these contributions complement each other and can be used in practice

Un nombre important et en constante augmentation de systèmes numériques nous entoure. Tablettes, smartphones et objets connectés ne sont que quelques exemples apparents de ces technologies omniprésentes, dont la majeure partie est enfouie, invisible à l'utilisateur. Les microprocesseurs, au cœur de ces systèmes, sont soumis à de fortes contraintes en ressources, sûreté de fonctionnement et se doivent, plus que jamais, de proposer une sécurité renforcée. La tâche est d'autant plus complexe qu'un tel système, par sa proximité avec l'utilisateur, offre une large surface d'attaque.Cette thèse, se concentre sur une propriété essentielle attendue pour un tel système, la confidentialité, le maintien du secret du programme et des données qu'il manipule. En effet, l'analyse du programme, des instructions qui le compose, est une étape essentielle dans la conception d'une attaque. D'autre part, un programme est amené à manipuler des données sensibles (clés cryptographiques, mots de passes, ...), qui doivent rester secrètes pour ne pas compromettre la sécurité du système.Cette thèse, se concentre sur une propriété essentielle attendue pour un tel système, la confidentialité, le maintien du secret du programme et des données qu'il manipule. Une première contribution de ces travaux est une méthode de chiffrement d'un code, basée sur le graphe de flot de contrôle, rendant possible l'utilisation d'algorithmes de chiffrement par flots, légers et efficaces. Protéger les accès mémoires aux données d'un programme s'avère plus complexe. Dans cette optique, nous proposons l'utilisation d'un chiffrement homomorphe pour chiffrer les données stockées en mémoire et les maintenir sous forme chiffrée lors de l'exécution des instructions. Enfin, nous présenterons l'intégration de ces propositions dans une architecture de processeur et les résultats d'évaluation sur logique programmable (FPGA) avec plusieurs programmes d'exemples
Embedded processors are today ubiquitous, dozen of them compose and orchestrate every technology surrounding us, from tablets to smartphones and a large amount of invisible ones. At the core of these systems, processors gather data, process them and interact with the outside world. As such, they are excepted to meet very strict safety and security requirements. From a security perspective, the task is even more difficult considering the user has a physical access to the device, allowing a wide range of specifically tailored attacks.Confidentiality, in terms of both software code and data is one of the fundamental properties expected for such systems. The first contribution of this work is a software encryption method based on the control flow graph of the program. This enables the use of stream ciphers to provide lightweight and efficient encryption, suitable for constrained processors. The second contribution is a data encryption mechanism based on homomorphic encryption. With this scheme, sensible data remain encrypted not only in memory, but also during computations. Then, the integration and evaluation of these solutions on Field Programmable Gate Array (FPGA) with some example programs will be discussed

Les systèmes embarqués sont de plus en plus intégrés dans les applications temps réel actuelles. Ils sont généralement constitués de composants matériels et logiciels profondément Intégrés mais hétérogènes. Ces composants sont développés sous des contraintes très strictes. En conséquence, le travail des ingénieurs de conception est devenu plus difficile. Pour répondre aux normes de haute qualité dans les systèmes embarqués de nos jours et pour satisfaire aux besoins quotidiens de l'industrie, l'automatisation du processus de développement de ces systèmes prend de plus en plus d'ampleur. Un défi majeur est de développer une approche automatisée qui peut être utilisée pour la vérification intégrée et la validation de systèmes complexes et hétérogènes.Dans le cadre de cette thèse, nous proposons une nouvelle approche compositionnelle pour la modélisation et la vérification des systèmes complexes décrits en langage SystemC. Cette approche est basée sur le modèle des SystemC Waiting State Automata (WSA). Les SystemC Waiting State Automata sont des automates permettant de modéliser le comportement abstrait des systèmes matériels et logiciels décrits en SystemC tout en préservant la sémantique de l'ordonnanceur SystemC au niveau des cycles temporels et au niveau des delta-cycles. Ce modèle permet de réduire la complexité de la modélisation des systèmes complexes due au problème de l'explosion combinatoire tout en restant fidèle au système initial. Ce modèle est compositionnel et supporte le rafinement. De plus, il est étendu par des paramètres temps ainsi que des compteurs afin de prendre en compte les aspects relatifs à la temporalité et aux propriétés fonctionnelles comme notamment la qualité de service. Nous proposons ensuite une chaîne de construction automatique des WSAs à partir de la description SystemC. Cette construction repose sur l'exécution symbolique et l'abstraction des prédicats. Nous proposons un ensemble d'algorithmes de composition et de réduction de ces automates afin de pouvoir étudier, analyser et vérifier les comportements concurrents des systèmes décrits ainsi que les échanges de données entre les différents composants. Nous proposons enfin d'appliquer notre approche dans le cadre de la modélisation et la simulation des systèmes complexes. Ensuite l'expérimenter pour donner une estimation du pire temps d'exécution (worst-case execution time (WCET)) en utilisant le modèle du Timed SystemC WSA. Enfin, on définit l'application des techniques du model checking pour prouver la correction de l'analyse abstraite de notre approche
Embedded systems are increasingly integrated into existing real-time applications. They are usually composed of deeply integrated but heterogeneous hardware and software components. These components are developed under strict constraints. Accordingly, the work of design engineers became more tricky and challenging. To meet the high quality standards in nowadays embedded systems and to satisfy the rising industrial demands, the automatization of the developing process of those systems is gaining more and more importance. A major challenge is to develop an automated approach that can be used for the integrated verification and validation of complex and heterogeneous HW/SW systems.In this thesis, we propose a new compositional approach to model and verify hardware and software written in SystemC language. This approach is based on the SystemC Waiting State Automata (WSA). The SystemC Waiting State Automata are used to model the abstract behavior of hardware or software systems described in SystemC. They preserve the semantics of the SystemC scheduler at the temporal and the delta-cycle level. This model allows to reduce the complexity of the modeling process of complex systems due to the problem of state explosion during modeling while remaining faithful to the original system. The SystemC waiting state automaton is also compositional and supports refinement. In addition, this model is extended with parameters such as time and counters in order to take into account further aspects like temporality and other extra-functional properties such as QoS.In this thesis, we propose a stepwise approach on how to automatically extract the SystemC WSAs from SystemC descriptions. This construction is based on symbolic execution together with predicate abstraction. We propose a set of algorithms to symbolically compose and reduce the SystemC WSAs in order to study, analyze and verify concurrent behavior of systems as well as the data exchange between various components. We then propose to use the SystemC WSA to model and simulate hardware and software systems, and to compute the worst cas execution time (WCET) using the Timed SystemC WSA. Finally, we define how to apply model checking techniques to prove the correctness of the abstract analysis

Detta examensarbete reder ut arbetsprinciperna för olika typer av hårddiskskrivskydd; hårdvaruskrivskydd, mjukvaruskrivskydd, hybridskrivskydd och bygelskrivskydd. Slutsatsen av utredningen är att endast hårdvaruskrivskydd Detta examensarbete reder ut arbetsprinciperna för olika typer av hårddiskskrivskydd; hårdvaruskrivskydd, mjukvaruskrivskydd, hybridskrivskydd och bygelskrivskydd. Slutsatsen av utredningen är att endast hårdvaruskrivskydd bedöms ha tillräckligt pålitliga skyddsprinciper, vilket motiveras av dess oberoende från både hårdvara och operativsystem.

Vidare undersöks hårdvaruskrivskyddet Image MASSter(TM) Drive Lock från Intelligent Computer Solutions (ICS). Några egentliga slutsatser gick inte dra av kretskonstruktionen, bortsett från att den är uppbyggd kring en FPGA (Xilinx Spartan-II, XC2S15) med tillhörande PROM (XC17S15APC).

En egenutvecklad idé till autenticieringsmetod för hårddiskkloner föreslås som ett tillägg till arbetet. Principen bygger på att komplettera hårddiskklonen med unik information om hårddisk såväl kloningsomständigheter, vilka sammanflätas genom XOR-operation av komponenternas hashsummor.Autenticieringsmetoden kan vid sjösättning möjligen öka rättsäkerheten för både utredarna och den som står misstänkt vid en brottsutredning.

Arbetet är till stora delar utfört vid och på uppdrag av Statens kriminaltekniska laboratorium (SKL) i Linköping.

碩士
輔仁大學
電子工程學系
90
In the operation of a remote measurement system, the response waveforms of the testing circuits connected with the interface circuit include the unwanted noise. Hence, in this paper, we propose the use of the digital signal processing method instead of our previously proposed method of using repeatedly measured response waveforms and software average methods. We pass the measured waveforms with their excessive noise through digital FIR filters to reduce the influence of noise at either the local or remote computers. Here, we use three types of the digital FIR filters: a FIR filter designed with a Hamming window, with a Kaiser window and an equiripple linear-phase FIR filter based on a Parks-McClellan algorithm. In addition, we compare their filtering performance that depends on the Minimum Mean Square Error (M.M.S.E.) with respect to the different filter order N. Our experiment results show that the higher filter order N is not positively in proportion to the better of M.M.S.E. However, all of the three filters can provide a range of improvement of from about 30 percent to 50 percent in M.M.S.E.. Finally, we compare the computation cost. The experimental results show that the computation cost is in proportion to the filter order N, but the computation cost is different from the varied digital filters. Finally, we use hardware structure to implement a function of the digital filter to verify the results of the software simulations.

Formal verification by model checking verifies whether a system satisfies some given correctness properties, and is intractable in general. We focus on several problems originating from the usage of model checking and from the inherent complexity of model checking itself. We propose approximation and iterative refinement techniques and demonstrate that they help in making these problems tractable on practical cases. Vacuity detection is one of the problems, relating to the trivial satisfaction of properties. A similar problem is query solving, useful in model exploration, when properties of a system are not fully known and are to be discovered rather than checked. Both of these problems have solution spaces structured as lattices and can be solved by model checking using those lattices. The lattices, in the most general formulation of these problems, are too complex to be implemented efficiently. We introduce a general approximation framework for model checking with lattices and instantiate this framework for the two problems, leading to algorithms and implementations that can obtain efficiently partial answers to the problems. We also introduce refinement techniques that consider incrementally larger lattices and compute even the partial answers gradually, to further abate the size explosion of the problems. Another problem we consider is the state-space explosion of model checking. The size of system models is exponential in the number of state variables and that renders model checking intractable. We consider systems composed of several components running concurrently. For such systems, compositional verification checks components individually to avoid composing an entire system. Model checking an individual component uses assumptions about the other components. Smaller assumptions lead to smaller verification problems. We introduce iterative refinement techniques that improve the assumptions generated by previous automated approaches. One technique incrementally refines the interfaces between components in order to obtain smaller assumptions that are sufficient to prove a given property. The smaller assumptions are approximations of the assumption that would be obtained without our interface refinement. Another technique computes assumptions as abstractions of components, as an alternative to current approaches that learn assumptions from counterexamples. Our abstraction refinement has the potential to compute smaller nondeterministic assumptions, in contrast to the deterministic assumptions learned by current approaches. We confirm experimentally the benefits of our new approximation and refinement techniques.

碩士
國立成功大學
工程科學系碩博士班
98
In recent years, digital information has been widely used in people’s daily life. Information security has become an important issue in digital life. In this thesis, we propose a new application, which combines hardware data encryption with software data hiding, and applies on a flash memory card through a card reader, aiming to achieve data protection. The 128-bit Advanced Encryption Standard (AES-128) is adopted in data encryption, and implemented on FPGA. To achieve a high-performance encryption, the hardware architecture fully utilizes Block RAMs in FPGA as data buffers, reducing the requirement for capacity of the external SRAM memory. In addition, the gold-key hidden technique is mainly implemented based on PC. For the reason that the progressive reconstruction property in JPEG 2000 image transmission, we embed the gold-key (or the identification of card reader) in the unimportant position, minimizing the loss of the quality caused by the hidden data, and accomplish the method in various applications. In this theory, we design the AES-128 by VerilogHDL, and implement it on Xilinx Spartan-3 XC3S400 FPGA. We also use JasPer as the basis of JPEG 2000 codec, and develop the GUI by Visual Studio 2008.

Les applications embarquées actuelles imposent des contraintes de plus en plus sévères. La puissance sans cesse croissante de calcul et de communication implique l'utilisation d'architectures multiprocesseurs, la portabilité implique des architectures monopuces et la faible consommation et faible coût impliquent des architectures dédiées. Ajouté à cela, les méthodes de conception évoluent moins vite que les possibilités technologiques d'intégration. Ainsi, une approche systématique partant d'un niveau d'abstraction plus élevé que le RTL est nécessaire pour réduire le temps de mise sur le marché et maîtriser la complexité.
Le sujet de cette thèse porte sur la mise en œuvre d'une nouvelle approche de conception systématique d'architectures multiprocesseurs monopuces dédiées à des application spécifiques.
Ainsi, un modèle architectural multiprocesseur générique est proposé. Ce modèle est modulaire, flexible et extensible, permettant de couvrir un large domaine d'applications. Les composants de traitement sont dissociés du réseau de communication via des interfaces génériques de communication jouant le rôle de coprocesseurs.
Un flot de conception complet est constitué de deux étapes principales. La première étape est l'étape d'exploration d'architecture. Concernant cette étape, une méthode d'estimation de performance au niveau système est proposée. Cette méthode permet une exploration rapide de l'espace de solutions architecturales pour trouver l'architecture système optimale pour l'application à concevoir. Le but de cette étape est de fixer les paramètres architecturaux (optimaux) dédiés à l'application. Ces paramètres sont utilisés dans la seconde étape –qui est l'étape d'implémentation– pour produire l'architecture RTL. Cette étape comporte trois types d'actions : la conception des composants logiciels, la conception des composants matériels et la conception du réseau de communication permettant d'intégrer les composants de base. Cette étape est réalisée de façon systématique basée sur l'instanciation et la configuration de composants dans une bibliothèque.
L'approche proposée permet de réduire significativement le temps de mise sur le marché de systèmes multiprocesseurs monopuces complexes. Plusieurs applications industrielles ont été réalisées pour valider et évaluer les performances de cette approche.

Кваліфікаційна робота присвячена проектуванню і розробці системи безпеки на прикладі інтернет-магазину «ГІГАБАЙТ+». Розроблена система дозволила підвищити рівень захищеності персональних даних, які зберігаються і обробляються в інформаційній системі підприємства. Метою дипломного проекту було розробка і реалізація політики інформаційної безпеки в мережі інтернет-магазину ІТ-послуг «ГІГАБАЙТ+». Для досягнення поставленої мети були вирішення такі завдання: – приведено короткий опис компанії; – проведено аналіз ризиків інформаційної безпеки; – приведено комплекс завдань, які підлягають подальшому вирішенню; – проведено аналіз і обгрунтування вибору системи безпеки; – описано впроваджувані програмно-апаратні засоби інформаційної безпеки, а також описано контрольний приклад застосування обраних засобів інформаційної безпеки.
The qualification thesis is devoted to to design and develop a security system on the example of the Gigabyte+online store. The developed system have increased the level of security of personal data that is stored and processed in the enterprise's information system. The aim of the diploma project was to develop and implement an information security policy in the network of the «Gigabyte+» online IT services store. To achieve this goal the following tasks have been solved: - a brief description of the company is provided; - an analysis of information security risks was carried out; – a set of tasks that are subject to further solution is given; - analysis and justification of the choice of security system was carried out; -the implemented information security software and hardware tools are described, as well as a control example of using the selected information security tools.
ПЕРЕЛІК УМОВНИХ ПОЗНАЧЕНЬ, СИМВОЛІВ, ОДИНИЦЬ, СКОРОЧЕНЬ І ТЕРМІНІВ .... 7 ВСТУП ... 8 1 ТЕОРЕТИЧНА ЧАСТИНА .... 10 1.1 Техніко-економічна характеристика предметної області та підприємства . 10 1.2 Аналіз ризиків інформаційної безпеки ... 14 1.3. Оцінка існуючих і планованих засобів захисту ... 20 1.4 Оцінка ризиків інформаційної безпеки .... 28 1.5 Висновки до розділу 1 ... 29 2 ДОСЛІДЖЕННЯ СИСТЕМИ ЗАБЕЗПЕЧЕННЯ ІНФОРМАЦІЙНОЇ БЕЗПЕКИ І ЗАХИСТУ ІНФОРМАЦІЇ НА ПІДПРИЄМСТВІ ...31 2.1 Характеристика комплексу задач, завдання та обґрунтування необхідності вдосконалення системи забезпечення інформаційної безпеки і захисту інформації на підприємстві .... 31 2.1.1. Вибір комплексу задач забезпечення інформаційної безпеки.... 31 2.1.2. Визначення місця проектованого комплексу завдань в комплексі завдань підприємства, деталізація завдань інформаційної безпеки і захисту інформації .... 35 2.2. Вибір захисних заходів... 38 2.2.1. Вибір організаційних заходів .... 38 2.2.2. Вибір інженерно-технічних заходів ...41 2.3 Висновки до розділу 2 ...43 3 ПРАКТИЧНА ЧАСТИНА. ПРОЕКТУВАННЯ ПРОГРАМНО-АПАРАТНОГО КОМПЛЕКСУ ІНФОРМАЦІЙНОЇ БЕЗПЕКИ І ЗАХИСТУ ІНФОРМАЦІЇ ПІДПРИЄМСТВА ... 44 3.1 Комплекс проектованих програмно-апаратних засобів забезпечення інформаційної безпеки і захисту інформації підприємства ...44 3.2 Контрольний приклад реалізації проекту і його опис ..67 3.3 Висновки до розділу 3 ... 72 4 Безпека життєдіяльності, основи хорони праці ..73 4.1 Вимоги до профілактичних медичних оглядів для працівників ПК. ... 73 4.2 Психофізіологічне розвантаження для працівників... 78 ВИСНОВКИ ... 80 СПИСОК ЛІТЕРАТУРНИХ ДЖЕРЕЛ ... 81

Les systèmes embarqués sont de plus en plus intégrés dans les applications temps réel actuelles. Ils sont généralement constitués de composants matériels et logiciels profondément Intégrés mais hétérogènes. Ces composants sont développés sous des contraintes très strictes. En conséquence, le travail des ingénieurs de conception est devenu plus difficile. Pour répondre aux normes de haute qualité dans les systèmes embarqués de nos jours et pour satisfaire aux besoins quotidiens de l'industrie, l'automatisation du processus de développement de ces systèmes prend de plus en plus d'ampleur. Un défi majeur est de développer une approche automatisée qui peut être utilisée pour la vérification intégrée et la validation de systèmes complexes et hétérogènes.Dans le cadre de cette thèse, nous proposons une nouvelle approche compositionnelle pour la modélisation et la vérification des systèmes complexes décrits en langage SystemC. Cette approche est basée sur le modèle des SystemC Waiting State Automata (WSA). Les SystemC Waiting State Automata sont des automates permettant de modéliser le comportement abstrait des systèmes matériels et logiciels décrits en SystemC tout en préservant la sémantique de l'ordonnanceur SystemC au niveau des cycles temporels et au niveau des delta-cycles. Ce modèle permet de réduire la complexité de la modélisation des systèmes complexes due au problème de l'explosion combinatoire tout en restant fidèle au système initial. Ce modèle est compositionnel et supporte le rafinement. De plus, il est étendu par des paramètres temps ainsi que des compteurs afin de prendre en compte les aspects relatifs à la temporalité et aux propriétés fonctionnelles comme notamment la qualité de service. Nous proposons ensuite une chaîne de construction automatique des WSAs à partir de la description SystemC. Cette construction repose sur l'exécution symbolique et l'abstraction des prédicats. Nous proposons un ensemble d'algorithmes de composition et de réduction de ces automates afin de pouvoir étudier, analyser et vérifier les comportements concurrents des systèmes décrits ainsi que les échanges de données entre les différents composants. Nous proposons enfin d'appliquer notre approche dans le cadre de la modélisation et la simulation des systèmes complexes. Ensuite l'expérimenter pour donner une estimation du pire temps d'exécution (worst-case execution time (WCET)) en utilisant le modèle du Timed SystemC WSA. Enfin, on définit l'application des techniques du model checking pour prouver la correction de l'analyse abstraite de notre approche
Embedded systems are increasingly integrated into existing real-time applications. They are usually composed of deeply integrated but heterogeneous hardware and software components. These components are developed under strict constraints. Accordingly, the work of design engineers became more tricky and challenging. To meet the high quality standards in nowadays embedded systems and to satisfy the rising industrial demands, the automatization of the developing process of those systems is gaining more and more importance. A major challenge is to develop an automated approach that can be used for the integrated verification and validation of complex and heterogeneous HW/SW systems.In this thesis, we propose a new compositional approach to model and verify hardware and software written in SystemC language. This approach is based on the SystemC Waiting State Automata (WSA). The SystemC Waiting State Automata are used to model the abstract behavior of hardware or software systems described in SystemC. They preserve the semantics of the SystemC scheduler at the temporal and the delta-cycle level. This model allows to reduce the complexity of the modeling process of complex systems due to the problem of state explosion during modeling while remaining faithful to the original system. The SystemC waiting state automaton is also compositional and supports refinement. In addition, this model is extended with parameters such as time and counters in order to take into account further aspects like temporality and other extra-functional properties such as QoS.In this thesis, we propose a stepwise approach on how to automatically extract the SystemC WSAs from SystemC descriptions. This construction is based on symbolic execution together with predicate abstraction. We propose a set of algorithms to symbolically compose and reduce the SystemC WSAs in order to study, analyze and verify concurrent behavior of systems as well as the data exchange between various components. We then propose to use the SystemC WSA to model and simulate hardware and software systems, and to compute the worst cas execution time (WCET) using the Timed SystemC WSA. Finally, we define how to apply model checking techniques to prove the correctness of the abstract analysis