We present the Hadley model, a formal descriptive model of input and output for modern computer operating systems. Our model is intentionally inspired by the Open Systems Interconnection model of networking; I/O as a process is defined as a set of translations between a set of computer-sensible forms, or layers, of information. To illustrate an initial application domain, we discuss the utility of the Hadley model and a potential associated I/O system as a tool for digital forensic investigators. To illustrate practical uses of the Hadley model we present the Hadley Specification Language, an essentially functional language designed to allow the translations that comprise I/O to be written in a concise format allowing for relatively easy verifiability. To further illustrate the utility of the language we present a read/write Microsoft DOS FAT12 and read-only Linux ext2 file system specification written in the new format. We prove the correctness of the read-only side of these descriptions. We present test results from operation of our HSL-driven system both in user mode on stored disk images and as part of a Linux kernel module allowing file systems to be read. We conclude by discussing future directions for the research.

Modern computer systems require efficient data transfers involving memory in order to get the best possible performance. However, even the most optimized CPUs take too long to access memory regions, which takes time away from doing the typical computations that a CPU is designed to do. To solve this, Direct Memory Access (DMA) is used, which allows peripherals and other hardware accelerators, such as stand-alone DMA Controllers (DMACs), to read and write memory without CPU intervention. However, DMA introduces security problems in which attackers are able to leak data and overwrite critical system components by bypassing typical operating system security mechanisms. This thesis presents a case study to model as well as verify DMA device driver code in HOL4, which is an interactive theorem prover (ITP) used for machine-checked verification. This thesis verifies parts of Intel's IXGBE X550 device driver, which is a complex, 10 Gbit Network Interface Card (NIC). This verification takes the first significant step towards proving that the DMA device driver configures the DMA device such that it preserves memory isolation, which ensures that only memory that is intended to be readable and writable will be accessed. This thesis also provides a formal method to verify that a loop terminates under all possible cases. This can be used to further verify the correctness of a DMA driver. These contributions allow for the overall increased security of memory when using DMA device drivers that are verified by this approach, leading to the hindrance of attacks on systems utilizing DMA. / Master of Science / Modern computer systems use Direct Memory Accesses (DMAs) in order to offload the CPU from doing memory transfers. However, this poses the problem that the CPU is not able to monitor every memory access made through DMA. This can lead to attackers utilizing vulnerabilities in the device drivers used to perform DMA operations. This thesis addresses this problem by modeling and verifying properties of a device driver that will prove that the driver configures DMA such that it is isolated. This thesis also models and verifies a loop to ensure that it terminates, further verifying the correctness of a function in a device driver. These contributions are significant because they allow for increased security of a computer system's memory, reducing the likelihood of attacks.

Approved for public release, distribution is unlimited / As more and more devices with a variety of capabilities are Internet-capable, device independence becomes a big issue when we would like the information that we request to be correctly displayed. This thesis introduces and compares how existing standards create a profile that describes the device capabilities to achieve the goal of device independence. After acknowledging the importance of device independence, this paper utilizes the idea to introduce a Device-Aware Network (DAN). DAN provides the infrastructure support for device-content compatibility matching for data transmission. We identify the major components of the DAN architecture and issues associated with providing this new network service. A Device-Aware Network will improve the network's efficiency by preventing unusable data from consuming host and network resources. The device profile is the key issue to achieve this goal. / Captain, Taiwan Army

Thesis (M.S.)--University of Texas at El Paso, 2008. / Title from title screen. Vita. CD-ROM. Includes bibliographical references. Also available online.

Thesis (MScEng)--University of Stellenbosch, 2003. / ENGLISH ABSTRACT: The Linux operating system and shared Ethernet are alternative technologies with the potential to reduce both the development time and costs of satellites as well as the supporting infrastructure. Modular satellites, ground stations and rapid proto typing testbeds also have a common requirement for distributed real-time computation. The identified technologies were investigated to determine whether this requirement could also be met. Various real-time extensions and modifications are currently available for the Linux operating system. A suitable open source real-time extension called Real-Time Application Interface (RTAI) was selected for the implementation of an experimental distributed real-time system. Experimental results showed that the RTAI operating system could deliver deterministic realtime performance, but only in the absence of non-real-time load. Shared Ethernet is currently the most popular and widely used commercial networking technology. However, Ethernet wasn't developed to provide real-time performance. Several methods have been proposed in literature to modify Ethernet for real-time communications. A token passing protocol was found to be an effective and least intrusive solution. The Real-Time Token (RTToken) protocol was designed to guarantee predictable network access to communicating real-time tasks. The protocol passes a token between nodes in a predetermined order and nodes are assigned fixed token holding times. Experimental results proved that the protocol offered predictable network access with bounded jitter. An experimental distributed real-time system was implemented, which included the extension of the RTAI operating system with the RTToken protocol, as a loadable kernel module. Real-time tasks communicated using connectionless Internet protocols. The Real-Time networking (RTnet) subsystem of RTAI supported these protocols. Under collision-free conditions consistent transmission delays with bounded jitter was measured. The integrated RTToken protocol provided guaranteed and bounded network access to communicating real-time tasks, with limit overheads. Tests exhibited errors in some of the RTAI functionality. Overall the investigated technologies showed promise in being able to meet the distributed real-time requirements of various applications, including those found in the satellite environment. / AFRIKAANSE OPSOMMING: Die Linux bedryfstelsel en gedeelde Ethernet is geïdentifiseer as potensiële tegnologieë vir satelliet bedryf wat besparings in koste en vinniger ontwikkeling te weeg kan bring. Modulêr ontwerpte satelliete, grondstasies en ontwikkeling platforms het 'n gemeenskaplike behoefte vir verspreide intydse verwerking. Verskillende tegnologieë is ondersoek om te bepaal of aan die vereiste ook voldoen kan word. Verskeie intydse uitbreidings en modifikasies is huidiglik beskikbaar vir die Linux bedryfstelsel. Die "Real-Time Application Interface" (RTAI) bedryfstelsel is geïdentifiseer as 'n geskikte intydse uitbreiding vir die implementering van 'n eksperimentele verspreide intydse stelsel. Eksperimentele resultate het getoon dat die RTAI bedryfstelsel deterministies en intyds kan opereer, maar dan moet dit geskied in die afwesigheid van 'n nie-intydse verwerkingslas. Gedeelde Ethernet is 'n kommersiële network tegnologie wat tans algemeen beskikbaar is. Die tegnologie is egter nie ontwerp vir intydse uitvoering nie. Verskeie metodes is in die literatuur voorgestelom Ethernet te modifiseer vir intydse kommunikasie. Hierdie ondersoek het getoon dat 'n teken-aangee protokol die mees effektiewe oplossing is en waarvan die implementering min inbreuk maak. Die "Real-Time Token" (RTToken) protokol is ontwerp om voorspelbare netwerk toegang tot kommunikerende intydse take te verseker. Die protokol stuur 'n teken tussen nodusse in 'n voorafbepaalde volgorde. Nodusse word ook vaste teken hou-tye geallokeer. Eksperimentele resultate het aangedui dat die protokol deterministiese netwerk toegang kan verseker met begrensde variasies. 'n Eksperimentele verspreide intydse stelsel is geïmplementeer. Dit het ingesluit die uitbreiding van die RTAI bedryfstelsel met die RTToken protokol; verpak as 'n laaibare bedryfstelsel module. Intydse take kan kommunikeer met verbindinglose protokolle wat deur die "Real-Time networking" (RTnet) substelsel van RTAI ondersteun word. Onder ideale toestande is konstante transmissie vertragings met begrensde variasies gemeet. Die integrasie van die RTToken protokol het botsinglose netwerk toegang aan kommunikerende take verseker, met beperkte oorhoofse koste as teenprestasie. Eksperimente het enkele foute in die funksionaliteit van RTAI uitgewys. In die algemeen het die voorgestelde tegnologieë getoon dat dit potensiaal het vir verskeie verspreide intydse toepassings in toekomstige satelliet en ook ander omgewings.

Made available in DSpace on 2014-06-12T15:49:42Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / Produtos eletrônicos modernos integram diversas funcionalidades, combinando mobilidade, poder computacional, uma alta capacidade para comunicação e flexibilidade de interfaceamento. No entanto, a integração dessas funcionalidades eleva a complexidade do projeto. O projeto de tais produtos inclui um sistema embarcado que, em geral, implementa suas funcionalidades em uma solução integrada de hardware e software. Uma plataforma de hardware baseada em processador permite a execução das funcionalidades do software do sistema. Os seus principais componentes são: processadores, memória, barramento e dispositivos periféricos. Modelos de simulação destes componentes podem ser obtidos e conectados para compor um modelo de plataforma virtual. Este modelo pode ser usado, ainda na fase inicial, para o desenvolvimento dos componentes de software: código dependente da plataforma, device drivers, funcionalidades do sistema operacional e aplicações do usuário. Nesse contexto, os dispositivos periféricos e os respectivos device drivers têm um papel importante, pois são responsáveis pelos diversos tipos de comunicação e interfaceamento com o mundo exterior, requisitos obrigatórios na maioria dos sistemas modernos. No entanto, o desenvolvimento de dispositivos periféricos não é uma tarefa simples, ainda que seja um modelo de simulação. Por outro lado, o desenvolvimento do driver depende da disponibilidade do modelo do dispositivo, além do tipo do processador e do sistema operacional. Essas dependências, portanto, podem acarretar atraso no tempo de desenvolvimento e afetar o custo do projeto. Assim, o desenvolvimento integrado e concorrente do dispositivo e do driver facilita a depuração, contribuindo para a eliminação de erro, além de reduzir o tempo total do projeto. Esse trabalho propõe uma abordagem para dar suporte ao desenvolvimento incremental e concorrente de device drivers e modelos de simulação do controlador de dispositivos, considerando diferentes níveis de detalhes dos modelos, o tipo do processador usado, bem como, a utilização de um sistema operacional. Para isso, uma linguagem específica do domínio é proposta para descrever características dos controladores e do device driver e, a partir dessa descrição, possibilitar que o controlador e os drivers sejam sintetizados. Para validar a proposta, uma plataforma baseada no processador Sparc foi desenvolvida e um porte do sistema operacional uclinux foi realizado. Alguns dispositivos periféricos e seus respectivos device drivers foram sintetizados tais como, UART, LCD display e dispositivos específicos para plataformas de computação reconfigurável. Esses componentes foram integrados à plataforma base e simulados para a validação dos componentes

The World Wide Web is becoming a basic infrastructure for a variety of services, and the increases in audience size and client network bandwidth create service demands that are outpacing server capacity. Web clusters are one solution to this need for highperformance, highly available web server systems. We are interested in load distribution techniques, specifically Layer-7 algorithms that are content-aware. Layer- 7 algorithms allow distribution control based on the specific content requested, which is advantageous for a system that offers highly heterogenous services. We examine the performance of the Client Aware Policy (CAP) on a Linux/Apache web cluster consisting of a single web switch that directs requests to a pool of dual-processor SMP nodes. We show that the performance advantage of CAP over simple algorithms such as random and round-robin is as high as 29% on our testbed consisting of a mixture of static and dynamic content. Under heavily loaded conditions however, the performance decreases to the level of random distribution. In studying SMP vs. uniprocessor performance using the same number of processors with CAP distribution, we find that SMP dual-processor nodes under moderate workload levels provide equivalent throughput as the same number of CPU’s in a uniprocessor cluster. As workload increases to a heavily loaded state however, the SMP cluster shows reduced throughput compared to a cluster using uniprocessor nodes. We show that the web cluster’s maximum throughput increases linearly with the addition of more nodes to the server pool. We conclude that CAP is advantageous over random or round-robin distribution under certain conditions for highly dynamic workloads, and suggest some future enhancements that may improve its performance.

Alors que la recherche sur la qualité du code des systèmes a connu un formidable engouement, les systèmes d’exploitation sont encore aux prises avec des problèmes de fiabilité notamment dus aux bogues de programmation au niveau des services noyaux tels que les pilotes de périphériques et l’implémentation des systèmes de fichiers. Des études ont en effet montré que chaque version du noyau Linux contient entre 600 et 700 fautes, et que la propension des pilotes de périphériques à contenir des erreurs est jusqu’à sept fois plus élevée que toute autre partie du noyau. Ces chiffres suggèrent que le code des services noyau n’est pas suffisamment testé et que de nombreux défauts passent inaperçus ou sont difficiles à réparer par des programmeurs non-experts, ces derniers formant pourtant la majorité des développeurs de services. Cette thèse propose une nouvelle approche pour le débogage et le test des services noyau. Notre approche est focalisée sur l’interaction entre les services noyau et le noyau central en abordant la question des “trous de sûreté” dans le code de définition des fonctions de l’API du noyau. Dans le contexte du noyau Linux, nous avons mis en place une approche automatique, dénommée Diagnosys, qui repose sur l’analyse statique du code du noyau afin d’identifier, classer et exposer les différents trous de sûreté de l’API qui pourraient donner lieu à des fautes d’exécution lorsque les fonctions sont utilisées dans du code de service écrit par des développeurs ayant une connaissance limitée des subtilités du noyau. Pour illustrer notre approche, nous avons implémenté Diagnosys pour la version 2.6.32 du noyau Linux. Nous avons montré ses avantages à soutenir les développeurs dans leurs activités de tests et de débogage. / Despite the existence of an overwhelming amount of research on the quality of system software, Operating Systems are still plagued with reliability issues mainly caused by defects in kernel-level services such as device drivers and file systems. Studies have indeed shown that each release of the Linux kernel contains between 600 and 700 faults, and that the propensity of device drivers to contain errors is up to seven times higher than any other part of the kernel. These numbers suggest that kernel-level service code is not sufficiently tested and that many faults remain unnoticed or are hard to fix bynon-expert programmers who account for the majority of service developers. This thesis proposes a new approach to the debugging and testing of kernel-level services focused on the interaction between the services and the core kernel. The approach tackles the issue of safety holes in the implementation of kernel API functions. For Linux, we have instantiated the Diagnosys automated approach which relies on static analysis of kernel code to identify, categorize and expose the different safety holes of API functions which can turn into runtime faults when the functions are used in service code by developers with limited knowledge on the intricacies of kernel code. To illustrate our approach, we have implemented Diagnosys for Linux 2.6.32 and shown its benefits in supporting developers in their testing and debugging tasks.

No description available.

This thesis deals with the communication on the PCI bus and the design of controllers for the PCI card with FPGA circuit. The introduction shows the functionality and structure of FPGA circuits, followed by description of the principle of communication through the PCI bus. After an analysis of the PCI the thesis describes a design of controllers for a target card and lets the reader get acquainted with its different parts. In the process of implementation carefully examines the structure and operation of individual blocks of PCI controller. In the following part the thesis shows the process of implementation and testing of the final solution using the educational card with FPGA circuit.