In this thesis, we investigate the applicability of the process algebraic formal method Communicating Sequential Processes (CSP) [Hoa85] to the development and analysis of safetycritical systems. We also investigate how these tasks might be aided by mechanical verification, which is provided in the form of the proof tool Failures-Divergences Refinement (FDR) [Ros94]. Initially, we build upon the work of [RWW94, Ros95], in which CSP treatments of the security property of non-interference are described. We use one such formulation to define a property called protection, which unifies our views of safety and security. As well as applying protection to the analysis of safety-critical systems, we develop a proof system for this property, which in conjunction with the opportunity for automated analysis provided by FDR, enables us to apply the approach to problems of a sizable complexity. We then describe how FDR can be applied to the analysis of mutual exclusion, which is a specific form of non-interference. We investigate a number of well-known solutions to the problem, and illustrate how such mutual exclusion algorithms can be interpreted as CSP processes and verified with FDR. Furthermore, we develop a means of verifying the faulttolerance of such algorithms in terms of protection. In turn, mutual exclusion is used to describe safety properties of geographic data associated with Solid State Interlocking (SSI) railway signalling systems. We show how FDR can be used to describe these properties and model interlocking databases. The CSP approach to compositionality allows us to decompose such models, thus reducing the complexity of analysing safety invariants of SSI geographic data. As such, we describe how the mechanical verification of Solid State Interlocking geographic data, which was previously considered to be an intractable problem for the current generation of mechanical verification tools, is computationally feasible using FDR. Thus, the goals of this thesis are twofold. The first goal is to establish a formal encapsulation of a theory of safety-critical systems based upon the relationship which exists between safety and security. The second goal is to establish that CSP, together with FDR, can be applied to the modelling of Solid State Interlocking geographic databases. Furthermore, we shall attempt to demonstrate that such modelling can scale up to large-scale systems.

This dissertation is aimed at defending against a range of internal threats, including eaves-dropping on network taps, placement of malware to capture sensitive information, and general insider threats to exfiltrate sensitive information. Although the threats and adversaries may vary, in each context where a system is threatened, decoys can be used to deny critical information to adversaries making it harder for them to achieve their target goal. The approach leverages deception and the use of decoy technologies to deceive adversaries and trap nefarious acts. This dissertation proposes a novel set of properties for decoys to serve as design goals in the development of decoy-based infrastructures. To demonstrate their applicability, we designed and prototyped network and host-based decoy systems. These systems are used to evaluate the hypothesis that network and host decoys can be used to detect inside attackers and malware. We introduce a novel, large-scale automated creation and management system for deploying decoys. Decoys may be created in various forms including bogus documents with embedded beacons, credentials for various web and email accounts, and bogus financial in- formation that is monitored for misuse. The decoy management system supplies decoys for the network and host-based decoy systems. We conjecture that the utility of the decoys depends on the believability of the bogus information; we demonstrate the believability through experimentation with human judges. For the network decoys, we developed a novel trap-based architecture for enterprise networks that detects "silent" attackers who are eavesdropping network traffic. The primary contributions of this system is the ease of injecting, automatically, large amounts of believable bait, and the integration of various detection mechanisms in the back-end. We demonstrate our methodology in a prototype platform that uses our decoy injection API to dynamically create and dispense network traps on a subset of our campus wireless network. We present results of a user study that demonstrates the believability of our automatically generated decoy traffic. We present results from a statistical and information theoretic analysis to show the believability of the traffic when automated tools are used. For host-based decoys, we introduce BotSwindler, a novel host-based bait injection sys- tem designed to delude and detect crimeware by forcing it to reveal itself during the ex- ploitation of monitored information. Our implementation of BotSwindler relies upon an out-of-host software agent to drive user-like interactions in a virtual machine, seeking to convince malware residing within the guest OS that it has captured legitimate credentials. To aid in the accuracy and realism of the simulations, we introduce a novel, low overhead approach, called virtual machine verification, for verifying whether the guest OS is in one of a predefined set of states. We provide empirical evidence to show that BotSwindler can be used to induce malware into performing observable actions and demonstrate how this approach is superior to that used in other tools. We present results from a user to study to illustrate the believability of the simulations and show that financial bait infor- mation can be used to effectively detect compromises through experimentation with real credential-collecting malware. We present results from a statistical and information theo- retic analysis to show the believability of simulated keystrokes when automated tools are used to distinguish them. Finally, we introduce and demonstrate an expanded role for decoys in educating users and measuring organizational security through experiments with approximately 4000 university students and staff.

Malicious attacks on computer systems attempt to obtain and maintain illicit control over the victim system. To obtain unauthorized access, they often exploit vulnerabilities in the victim system, and to maintain illicit control, they apply various hiding techniques to remain stealthy. In this dissertation, we discuss and present solutions for two classes of security problems: TOCTTOU (time-of-check-to-time-of-use) and K-Queue. TOCTTOU is a vulnerability that can be exploited to obtain unauthorized root access, and K-Queue is a hiding technique that can be used to maintain stealthy control of the victim kernel. The first security problem is TOCTTOU, a race condition in Unix-style file systems in which an attacker exploits a small timing gap between a file system call that checks a condition and a use kernel call that depends on the condition. Our contributions on TOCTTOU include: (1) A model that enumerates the complete set of potential TOCTTOU vulnerabilities; (2) A set of tools that detect TOCTTOU vulnerabilities in Linux applications such as vi, gedit, and rpm; (3) A theoretical as well as an experimental evaluation of security risks that shows that TOCTTOU vulnerabilities can no longer be considered "low risk" given the wide-scale deployment of multiprocessors; (4) An event-driven protection mechanism and its implementation that defend Linux applications against TOCTTOU attacks at low performance overhead. The second security problem addressed in this dissertation is kernel queue or K-Queue, which can be used by the attacker to achieve continual malicious function execution without persistently changing either kernel code or data, which prevents state-of-the-art kernel integrity monitors such as CFI and SBCFI from detecting them. Based on our successful defense against a concrete instance of K-Queue-driven attacks that use the soft timer mechanism, we design and implement a solution to the general class of K-Queue-driven attacks, including (1) a unified static analysis framework and toolset that can generate specifications of legitimate K-Queue requests and the checker code in an automated way; (2) a runtime reference monitor that validates K-Queue invariants and guards such invariants against tampering; and (3) a comprehensive experimental evaluation of our static analysis framework and K-Queue Checkers.

Orientador: Paulo Licio de Geus / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-07T00:53:39Z (GMT). No. of bitstreams: 1 Carbone_Martimd'OreyPosserdeAndrade_M.pdf: 997778 bytes, checksum: 199d19777ac058e5c7dcecaa5c43639f (MD5) Previous issue date: 2006 / Resumo: O crescimento alarmante da quantidade e da sofisticação dos ataques aos quais estão sujeitos os sistemas computacionais modernos traz à tona a necessidade por novos sistemas de segurança mais eficientes. Na natureza, há um sistema biológico que realiza esta tarefa com notável eficácia: o sistema imunológico humano. Este sistema é capaz de garantir a sobrevivência de um ser humano por décadas, além de ser capaz de aprender sobre novas ameaças e criar defesas para combatê-Ias. Sua eficácia, somada à semelhança entre o cenário da segurança biológica e o da segurança computacional, motivou a criação do projeto Imuno, cujo objetivo é a construção de um sistema de segurança para computadores baseado nos princípios do sistema imunológico humano. Após o estudo inicial, a modelagem conceitual do sistema e a implementação de protótipos restritos de certas funcionalidades do sistema Imuno, este trabalho tem como objetivo avançar rumo à construção de um sistema de segurança imunológico completo, de escopo geral. Para isso, torna-se necessária a implementação de uma framework em nível de sistema operacional, que suporte as funcionalidades relacionadas à prevenção, detecção e resposta que serão utilizadas por este sistema de segurança. Projetada para o kernel Linux 2.6, esta framework é composta por algumas frameworks pré-existentes, como Lima Security Modules (LSM), Netfilter, Class-based Kernel Resource Management (CKRM), BSD Secure Levels (SEClvl) e UndoFS, ajustadas de acordo com os requisitos levantados para a framework; e somadas a uma nova arquitetura de ganchos multifuncionais. Esta arquitetura expande a infraestrutura nativa dos ganchos LSM, tornando-os flexíveis e genéricos o bastante para serem utilizados com outras funcionalidades de segurança além de controle de acesso, como detecção e resposta, além de poderem ser controlados do espaço de usuário em tempo real. Um protótipo foi implementado para a versão 2.6.12 do Linux e submetido a testes, visando avaliar tanto o impacto de desempenho gerado como também o seu comportamento em um cenário de ataque simulado. Os resultados destes testes são expostos no final deste trabalho, junto com as conclusões gerais sobre o projeto e propostas de extensão / Abstract: The alarming growth in the quantity and the sophistication of the attacks that threaten modem computer systems shows the need for new, more efticient security systems. In nature, there is a biological system that accomplishes this task with a remarkable efticiency: the human immune system. Not only this system is capable of assuring the survival of a human being for decades; it is also capable of learning about new threats and creating defenses to fight them. Its efticiency, combined with the similarity that exists between the biological and the computer security problems, has motivated the creation of the Imuno project, whose goal is the construction of a computer security system based on the principIes of the human immune system. After initial studies, the system's conceptual modeling and the implementation of prototypes of certain Imuno functionalities, this project's goal is to advance towards the construction of a complete, general scope immune security system. In order to accomplish that, the implementation of an operating system leveI framework that supports the prevention, detection and response security functionalities to be used by such a system is necessary. Designed for the 2.6 Linux kernel, this framework is composed of several pre-existing frameworks, such as Linux Security Modules (L8M), Netfilter, Class-based Kernel Resource Management (CKRM), BSD Secure Levels (8EClvl) and UndoFS, adjusted according to the framework requirements; and supplemented by a new multifunctional hook architecture. This architecture expands L8M's native hook infrastructure, making them flexible and generic enough to be used by other security functionalities beyond access control, such as detection and response, and also capable of being controlled from userspace in real-time. A prototype has been implemented for Linux version 2.6.12 and submitted to various tests, aiming to evaluate the performance overhead it creates and its behavior in a simulated attack situation. These tests' results are shown at the end of this document, along with a general conclusion about the project and extension proposals / Mestrado / Mestre em Ciência da Computação