Trusted Execution Environments (TEE) are ubiq-uitous. They form the highest privileged software component of the platform with full access to the system and associated devices. However, vulnerabilities have been found in deployed TEEs allowing an attacker to gain complete control. Despite the progress made in fully-verified software systems, few deployed TEEs are fully-verified, due to the high cost of verification. Instead of aiming for full-functional correctness, this paper proposes a formal framework and approach that leverages com-partmentalization at the source level to bring security-relevant properties verified at the source level down to the binary via existing certified compilers. The benefit of our approach is the relative low cost of verification: developers can use existing automated program verification tools and certified compilers. Our case studies demonstrate how security properties verified on two open-source TEEs at the source level can be pushed down to the compiled code by using an off-the-shelf certified compiler.

Today’s edge networks continue to see an increasing number of deployed IoT devices. These IoT devices aim to increase productivity and efficiency; however, they are plagued by a myriad of vulnerabilities. Industry and academia have proposed protecting these devices by deploying a “bolt-on” security gateway to these edge networks. The gateway applies security protections at the network level. While security gateways are an attractive solution, they raise a fundamental concern: Can the bolt-on security gateway be trusted? This paper identifies key challenges in realizing this goal and sketches a roadmap for providing trust in bolt-on edge IoT security gateways. Specifically, we show the promise of using a micro-hypervisor driven approach for delivering practical (deployable today) trust that is catered to both end-users and gateway vendors alike in terms of cost, generality, capabilities, and performance. We describe the challenges in establishing trust on today’s edge security gateways, formalize the adversary and trust properties, describe our system architecture, encode and prove our architecture trust properties using the Alloy formal modeling language. We foresee our trustworthy security gateway architecture becoming a practical and extensible formal foundation towards realizing robust trust properties on today’s edge security gateway implementations.

Verifying complex Cyber-Physical Systems (CPS) is increasingly important given the push to deploy safety-critical autonomous features. Unfortunately, traditional verification methods do not scale to the complexity of these systems and do not provide systematic methods to protect verified properties when not all the components can be verified. To address these challenges, this paper proposes a real-time mixed-trust computing framework that combines verification and protection. The framework introduces a new task model, where an application task can have both an untrusted and a trusted part. The untrusted part allows complex computations supported by a full OS with a realtime scheduler running in a VM hosted by a trusted hypervisor. The trusted part is executed by another scheduler within the hypervisor and is thus protected from the untrusted part. If the untrusted part fails to finish by a specific time, the trusted part is activated to preserve safety (e.g., prevent a crash) including its timing guarantees. This framework is the first allowing the use of untrusted components for CPS critical functions while preserving logical and timing guarantees, even in the presence of malicious attackers. We present the framework design and implementation along with the schedulability analysis and the coordination protocol between the trusted and untrusted parts. We also present our Raspberry Pi 3 implementation along with experiments showing the behavior of the system under failures of untrusted components, and a drone application to demonstrate its practicality.

Robust security on a commodity low-cost and popular computing platform is a worthy goal for today's Internet of Things (IoT) and embedded ecosystems. We present the first practical security architecture on the Raspberry PI (PI), a ubiquitous and popular low-cost compute module. Our architecture and framework - called UBERPI - focuses on three goals which are keys to achieving practical security: commodity compatibility (e.g., runs unmodified Raspbian/Debian Linux) and unfettered access to platform hardware, performance (avg. 2%-6% overhead), and low trusted computing base and complexity (modular 5544 SLoC).We present a full implementation followed by a comprehensive evaluation and lessons learned. We believe that our contributions and findings elevate the PI into a next generation, secure, low-cost IoT embedded computing platform.

We present OASIS, a CPU instruction set extension for externally verifiable initiation, execution, and termination of an isolated execution environment with a trusted computing base consisting solely of the CPU. OASIS leverages the hardware components available on commodity CPUs to achieve a low-cost, low-overhead design.

We present the design, implementation, and verification of XMHF- an eXtensible and Modular Hypervisor Framework. XMHF is designed to achieve three goals -- modular extensibility, automated verification, and high performance. XMHF includes a core that provides functionality common to many hypervisor-based security architectures and supports extensions that augment the core with additional security or functional properties while preserving the fundamental hypervisor security property of memory integrity (i.e., ensuring that the hypervisor's memory is not modified by software running at a lower privilege level). We verify the memory integrity of the XMHF core -- 6018 lines of code -- using a combination of automated and manual techniques. The model checker CBMC automatically verifies 5208 lines of C code in about 80 seconds using less than 2GB of RAM. We manually audit the remaining 422 lines of C code and 388 lines of assembly language code that are stable and unlikely to change as development proceeds. Our experiments indicate that XMHF's performance is comparable to popular high-performance general-purpose hypervisors for the single guest that it supports.

Outsourced computation services should ideally only charge customers for the resources used by their applications. Unfortunately, no verifiable basis for service providers and customers to reconcile resource accounting exists today. This leads to undesirable outcomes for both providers and consumers-providers cannot prove to customers that they really devoted the resources charged, and customers cannot verify that their invoice maps to their actual usage. As a result, many practical and theoretical attacks exist, aimed at charging customers for resources that their applications did not consume. Moreover, providers cannot charge consumers precisely, which causes them to bear the cost of unaccounted resources or pass these costs inefficiently to their customers.

A detailed understanding of the behavior of exploits and malicious software is necessary to obtain a comprehensive overview of vulnerabilities in operating systems or client applications, and to develop protection techniques and tools. To this end, a lot of research has been done in the last few years on binary analysis techniques to efficiently and precisely analyze code. Most of the common analysis frameworks are based on software emulators since such tools offer a fine-grained control over the execution of a given program. Naturally, this leads to an arms race where the attackers are constantly searching for new methods to detect such analysis frameworks in order to successfully evade analysis.

Much effort has been spent to reduce the software Trusted Computing Base (TCB) of modern systems. However, there remains a large and complex hardware TCB, including memory, peripherals, and system buses. There are many stronger, but still realistic, adversary models where we need to consider that this hardware may be malicious or compromised. Thus, there is a practical need to determine whether we can achieve secure program execution in the presence of not only malicious software, but also malicious hardware.

This paper extends VAMPiRE, a stealth breakpoint framework specifically tailored for microscopic malware analysis. Stealth breakpoints are designed to provide unlimited number of code, data and I/O breakpoints that cannot be detected or countered. However, in this paper we present several attacks that can be used to detect and counter VAMPiRE. We then present a solution towards preventing such attacks in the form of a new breakpoint framework named Galanus. Galanus also adds support for legacy I/O breakpoints in kernel-mode, an important feature required to analyze keyloggers, BIOS flashers, CMOS updaters and rootkits. We also evaluate Galanus, comparing it to VAMPiRE in the context of a few real-world malware.

Malware or malicious code is a rapidly evolving threat to the computing community. Zero-day malware are exploiting vulnerabilities very soon after being discovered and are spreading quickly. However, anti-virus tools, which are the most widely used countering mechanism, are unable to cope with this. They are based on signatures which need to be computed for new malware strains. After a new malware strikes and before the signature is found allows sufficient time for the malware to perform its damage. We propose a new framework, codenamed MalTRAK, which, when deployed on a clean system, guarantees that any effects of a known or unknown malware can always be reversed and the system can be restored back to a prior clean state. Our framework also maintains detailed dependency lists of system operations which can be used for further forensic analysis. We are able to achieve this without imposing any restrictions on the nature of programs that can be executed by the user and without the user noticing any perceptible system slowdown due to the framework. Furthermore, we are able to track modifications to the system at a level that ensures that we can always monitor any changes to the system state even if a malware modifies the system during execution. We implemented and evaluated MalTRAK on Windows, using 8 known malware assuming they were unknown strains. We then compared our results with two popular commercial anti-virus tools. We were able to successfully restore all the effects of the 8 malware, while the commercial tools, on an average were only able to restore 36% of all their effects put together. For one of the malware samples, the commercial tools could only detect it but could not repair any of its damage. Further, for two of the malware samples, the commercial tools were completely unable to detect or restore any of their effects. Our results show that signature based mechanisms in addition to not being able to prevent infection by new malware strains, are not very effective in removing an infection even after a signature has been developed. Our experience shows that non-signature based approaches, such as MalTRAK, are the next step towards combating the threat of ever-evolving malware.

Fine-grained code analysis in the context of malware is a complex and challenging task that provides insight into malware code-layers (polymorphic/metamorphic), its data encryption/decryption engine, its memory layout etc., important pieces of information that can be used to detect and counter the malware and its variants. Current research in fine-grained code analysis can be categorized into static and dynamic approaches. Static approaches have been tailored towards malware and allow exhaustive fine-grained malicious code analysis, but lack support for self-modifying code, have limitations related to code-obfuscations and face the undecidability problem. Given that most if not all malware employ self-modifying code and code-obfuscations, poses the need to analyze them at runtime using dynamic approaches. However, current dynamic approaches for fine-grained code analysis are not tailored specifically towards malware and lack support for multithreading, self-modifying/self-checking code and are easily detected and countered by ever-evolving anti-analysis tricks employed by malware. To address this problem, we propose a powerful dynamic fine-grained malicious code analysis framework, codenamed Cobra, to combat malware that are becoming increasingly hard to analyze. Our goal is to provide a stealth, efficient, portable and easy-to-use framework supporting multithreading, self-modifying/self-checking code and any form of code obfuscation in both user- and kernel-mode on commodity operating systems. Cobra cannot be detected or countered and can be dynamically and selectively deployed on malware specific code-streams while allowing other code-streams to execute as is. We also illustrate the framework utility by describing our experience with a tool employing Cobra to analyze a real-world malware

Microscopic analysis of malicious code (malware) requires the aid of a variety of powerful tools. Chief among them is a debugger that enables runtime binary analysis at an instruction level. One of the important services provided by a debugger is the ability to stop execution of code at an arbitrary point during runtime, using breakpoints. Software breakpoints support an unlimited number of breakpoint locations by changing the code being debugged so that it can be interrupted during runtime. Most, if not all, malware are very sensitive to code modification with self-modifying and/or self-checking (SM-SC) capabilities, rendering the use of software breakpoints limited in their scope. Hardware breakpoints supported by the underlying processor, on the other hand, use a subset of the processor register set and exception mechanisms to provide breakpoints that do not entail code modification. This makes hardware breakpoints the most powerful breakpoint mechanism for malware analysis. However, current processors provide a very limited number of hardware breakpoints (typically 2-4 locations). Thus, a serious restriction is imposed on the debugger to set a desired number of breakpoints without resorting to the limited alternative of software breakpoints. Also, with the ever evolving nature of malware, there are techniques being employed that prevent the use of hardware breakpoints. This calls for a new breakpoint mechanism that retains the features of hardware breakpoints while providing an unlimited number of breakpoints, which cannot be detected or countered. In this paper, we present the concept of stealth breakpoints and discuss the design and implementation of VAMPiRE, a realization of this concept. VAMPiRE cannot be detected or countered and provides unlimited number of breakpoints to be set on code, data, and I/O with the same precision as that of hardware breakpoints. It does so by employing a subtle combination of simple stealth techniques using virtual memory and hardware single-stepping mechanisms that are available on all processors, old and new. This technique makes VAMPiRE portable to any architecture, providing powerful breakpoint ability similar to hardware breakpoints for microscopic malware analysis