Alright. Every so often I scoop up papers and throw them in folders. It's been disorganized past year or two. Here's some I've dug up recently, a few older ones i ran into again, and a useful one or two someone might not have seen. Apologize for the formatting: just happened when i was copy/pasting stuff and i had too little time to fix it. Latest Research (These I posted before. I think they're all great, ground-up redesign ideas. SecureMe's hardware assistance and SAFE's tagged architecture are similar to stuff Ive proposed here over time. Enough researchers gravitate toward a solution it might be worth extra effort, eh?) Preliminary design of the SAFE Platform 2011 DeHon et al. (They've since made plenty of progress.See crash-safe.org.) Part of DARPA Clean Slate. Typing/tagging is applied at hardware word level in processor, with a tag unit running parallel to execution. TPM is included. This combo I like most about project. A "concreteware" layer "wraps hardware into an abstract machine." "Userware" runs on top of it. They use high-level, mostly type-safe language called Breeze for all software. A verifiable subset called Tempest is what they'll do systems programming in. Some of that was probably inspired by Pragmatica Project, House, Habit, etc. SecureME: A Hardware-Software Approach to Full System Security (2011) Chhabra et al. "We propose SecureME, a hardware-software mechanism that provides such a secure computing environment. SecureME protects an application from hardware attacks by using a secure pro- cessor substrate, and also from the Operating System (OS) through memory cloaking, permission paging, and system call protection. Memory cloaking hides data from the OS but allows the OS to perform regular virtual memory man- agement functions, such as page initialization, copying, and swapping. Permission paging extends the OS paging mech- anism to provide a secure way for two applications to es- tablish shared pages for inter-process communication. Fi- nally, system call protection applies spatio-temporal pro- tection for arguments that are passed between the applica- tion and the OS. Based on our performance evaluation us- ing microbenchmarks, single-program workloads, and multi- programmed workloads, we found that SecureME only adds a small execution time overhead compared to a fully un- protected system. Roughly half of the overheads are con- tributed by the secure processor substrate. SecureME also incurs a negligible additio " Bootstrapping Trust in Commodity Computers 2010 Parno It's basically a detailed look at many TPM use cases, tech's, bootstrappings, etc. Good paper for that as TPM use is going up. (end of that group of papers) A High-Performance, Low-Overhead Microarchitecture for Secure Program Execution (2012) Kanuparthi et al. This is essentially dynamic integrity checks on data within the processor as the system runs. This usually slows things down. Their improvement is to treat the calculations transactionally, with a rollback upon failure. Only for static code. 1.66% performance overhead. Safe Loading - A Foundation for Secure Execution of Untrusted Programs (2012) Payer et al. Another nice piece of work from ETH Zurich guys. I regularly check on them b/c they do a lot of practical research. This paper is concerned with issues re. the standard loader (ld.so). They combine a secure loader with SFI-style sandboxing. Dissent in Numbers: Making Strong Anonymity Scale (2012) Wolinsky et al Navy's CHACS lab is at it again! From abstract: "Dissent derives its scalability from a client/server architecture, in which many unreliable clients depend on a smaller and more robust, but administratively decentralized, set of servers. Clients trust only that at least one server in the set is hon-est, but need not know or choose which server to trust.... Further, Dissent’s servers can unilaterally ensure progress, even if clients respond slowly or disconnect at arbitrary times, ensuring robust-ness against client churn, tail latencies, and DoS attacks" Tested with 5,000 participants with relatively low latencies. Enforcing User-Space Privilege Separation with Declarative Architectures (2012) Niu and Tan Uses uPro to seperate software into communicating protection domains. Implemented totally in userspace w/out kernel modifications. Developers use declarative language to describe app's security architecture, sparing them crap like SELinux policies. The "related work" section is nice b/c it has a bunch of other stuff for people to look into, esp SFI-related stuff. Fides: Selectively Hardening Software Application Components against Kernel-level or Process-level Malware (2012) Strackx and Piessens "(1) a run-time security architecture that can efficiently protect fine-grained software modules executing on a stan- dard operating system, and (2) a compiler that compiles standard C source code modules to such protected binary modules." Doesn't prevent software vulnerabilities necessarily. Just stops vulnerabilities in one compartment from affecting another arbitrarily and forces communications through certain entry points. (Many papers are doing something like this. It's starting to get redundant haha.) InkTag: Secure Applications on an Untrusted Operating System (2013) Hoffman et al "We introduce paraverification, a technique that simplifies the InkTag hypervisor by forcing the untrusted operating system to participate in its own verification. Attribute-based access control allows trusted applications to create decentralized access control policies. InkTag is also the first system of its kind to ensure consistency between secure data and metadata, ensuring recover- ability in the face of system crashes." INVISIOS: A Lightweight, Minimally Intrusive Secure Execution Environment 2012 Arora et al (Booz allen hamilton, intel, princeton and purdue were involved here) Mainly to be applied to embedded systems and SOC's. Quote: " we propose INVISIOS: a lightweight, minimally intrusive hardware-software architecture to make the execution of security-critical software invisible to the OS, and hence protected from its vulnerabil- ities. The INVISIOS software architecture encapsulates the security-critical software into a self-contained software module. While this module is part of the kernel and is run with kernel-level privileges, its code, data, and execution are transparent to and protected from the rest of the kernel. The INVISIOS hardware architecture consists of simple add-on hardware components that are responsible for bootstrapping the se- cure core, ensuring that it is exercised by applications in only permitted ways, and enforcing the isolation of its code and data. " Lessons from VAX/SVS for high-assurance VM systems (2012) Lipner, Jaeger and Zurko Heck yes! Another look at one of my favorite old Orange Book A1 class designs, the VAX Security Kernel. Paul Karger, a now deceased heavyweight in high assurance, contributed to it. There was already a lessons learned paper on it but this paper has worthwhile extra points. SAFER PATH: Security Architecture using Fragmented Execution and Replication for Protection Against Trojaned Hardware by Beaumont et al "We protect the integrity of the computation, the confidentiality of data being processed and ensure system availability. By combining a small Trusted Computing Base with Commercial-Off-The-Shelf processing elements, we are able to protect computation from the effects of arbitrary Hardware Trojans." Pasture: Secure Offline Data Access Using Commodity Trusted Hardware by Kolta et al 2013 "Pasture leverages commodity trusted hardware to provide two important safety properties: access- undeniability (a user cannot deny any offline data ac- cess obtained by his device without failing an audit) and verifiable-revocation (a user who generates a verifiable proof of revocation of unaccessed data can never access that data in the future)." CRUST: Cryptographic Remote Untrusted Storage without Public Keys 2012 Geron & Wool "CRUST is intended to be layered over insecure network file systems without changing the ex- isting systems. In our approach, data at rest is kept en- crypted, and data integrity and access control are provided by cryptographic means. Our design completely avoids public-key cryptography operations and uses more effi- cient symmetric-key alternatives to achieve improved per- formance. " A Survey of Virtualization Technologies Focusing on Untrusted Code Execution 2012 Zhao et al Looks at a bunch of them. Useful since it's a common trend in research. Declarative, Temporal, and Practical Programming with Capabilities (2013) Some people here have posted on Capsicum for freebsd. This paper describes capweave: a tool that combines a LLVM-based program with a developer-defined policy to rewrite a program to use Capsicum. Deserves mention b/c it's tech that makes security easy on developers and legacy applications. That's always good. Memory errors - past present and future 2012 van der veen This paper was a very good read. Sums up various strategies for attacking software via memory over time. I guess heap spraying and ROP are still my favorites. (Or maybe my old UseCacheAsCovertChannel strategy.) Practical Control Flow Integrity & Randomization for Binary Executables 2013 Zhang et al. Nice: "We propose a new practical and realistic protection method called CCFIR (Compact Control Flow Integrity and Random- ization), which addresses the main barriers to CFI adoption. CCFIR collects all legal targets of indirect control-transfer in- structions, puts them into a dedicated “Springboard section” in a random order, and then limits indirect transfers to flow only to them. Using the Springboard section for targets, CCFIR can validate a target more simply and faster than traditional CFI, and provide support for on-site target-randomization as well as better compatibility. Based on these approaches, CCFIR can stop control-flow hijacking attacks including ROP and return- into-libc." An Architecture for Enforcing End-to-End Access Control Over Web Applications 2010 Hicks et al. I've done custom browser clients in the past so this peaked my interest. They make it easier by using COTS components. "We overcome the limitations of traditional MAC systems, imple- mented solely at the operating system layer, by unifying MAC enforcement across virtual machine, operating system, network- ing and application layers. We implement our architecture us- ing Xen virtual machine management, SELinux at the oper- ating system layer, labeled IPsec for networking and our own label-enforcing web browser, called FlowwolF." Secure multi-execution through static program transformation: extended version 2012 Barthe et al. "In a nutshell, SME enforces security by running one execution of the program per security level, and by reinterpreting input/output operations w.r.t. their associated se- curity level. SME is sound, in the sense that the execution of a program under SME is non-interfering, and precise, in the sense that for programs that are non-interfering in the usual sense, the semantics of a program under SME coincides with its standard se- mantics. A further virtue of SME is that its core idea is language- independent; it can be applied to a broad range of languages." "we develop an alter- native approach where the e ect of SME is achieved through pro- gram transformation, without modi cations to the runtime, thus supporting server-side deployment on the web. We show on an ex- emplary language with input/output and dynamic code evaluation (modeled after JavaScript's eval) that our transformation is sound and precise. The crux of the proof is a simulation between the execution of the transformed program and the SME execution of the original program. This proof has been machine-checked using the Agda proof assistant. We also report on prototype implemen- tations for a small fragment of Python and a substantial subset of JavaScript." A Secure User Interface for Web Applications Running Under an Untrusted Operating System (2010) Li et al "In this paper, a secure user interface running under an untrusted OS is proposed, which is independent of the OS/applications and has a very small code base size. This secure user interface attests itself to the remote server and then handles the sensitive input and output by itself, bypassing the OS kernel and web applications. It utilizes network software stacks in the OS, however, the sensitive information is cryptographically protected before being revealed to the potentially malicious OS. This ensures the confidentiality and integrity of the sensitive information. Using this secure user interface, even while running under untrusted OS/applications, the user’s sensitive input, private output, and transaction integrity can be protected." Lessons learned building the caernarvon high-assurance operating system 2011 Karger et al. A smart card OS built for EAL7 by legend Paul Karger (and a team of others). He died a bit after this. The paper explores the issues, tradeoffs and benefits of their foray into EAL7 software design. Incremental development to sustain a project is the No 1 takeaway here. Fine-Grained Privilege Separation for Web Applications (2010) Krishnamurthy et al. "We present a programming model for building web applications with security properties that can be confidently verified during a security review. In our model, applications are divided into iso- lated, privilege-separated components, enabling rich security poli- cies to be enforced in a way that can be checked by reviewers. In our model, the web framework enforces privilege separation and isolation of web applications by requiring the use of an object- capability language and providing interfaces that expose limited, explicitly-specified privileges to application components. This ap- proach restricts what each component of the application can do and quarantines buggy or compromised code. It also provides a way to more safely integrate third-party, less-trusted code into a web appli- cation. We have implemented a prototype of this model based upon the Java Servlet framework and used it to build a webmail applica- tion. " Small Trusted Primitives for Dependable Systems 2011 Maniatis and Chun Another for TPM fans. Paper focuses on building security cases on a few trusted (or attested) components. TrustVisor - efficient TCB reduction and attestation 2010 McCune et al. From the team that brough you the well-designed SecVisor concept: "We present TrustVisor, a special-purpose hypervisor that provides code integrity as well as data integrity and secrecy for selected portions of an application. TrustVisor achieves a high level of security, first because it can protect sensitive code at a very fine granularity, and second because it has a very small code base (only around 6K lines of code) that makes verification feasible. TrustVisor can also attest the ex- istence of isolated execution to an external entity. We have implemented TrustVisor to protect security-sensitive code blocks while imposing less than 7% overhead on the legacy OS and its applications in the common case." Verified Security for Browser Extensions (microsoft) Guha et al. Who said Microsoft don't innovate? ;) "This paper presents I BEX, a new framework for authoring, analyzing, verifying, and deploying secure browser extensions. Our approach is based on using type-safe, high-level languages to program extensions against an API providing access to a variety of browser features. We propose using Datalog to specify fine-grained access control and data flow policies to limit the ways in which an extension can use this API, thus restricting its privilege over security-sensitive web content and browser resources. We formalize the semantics of policies in terms of a safety property on the execution of extensions and develop a verification methodology that allows us to statically check extensions for policy compliance. Additionally, we provide visualization tools to assist with policy analysis, and compilers to translate extension source code to either .NET bytecode or JavaScript, facilitating cross-browser deployment of extensions." Provable Protection of Confidential Data in Microkernel-Based Systems 2011 Dresden Group For microkernel based TCB's. Paper gives a "budget-enforcing, fixed-priority scheduler that provably eliminates covert timing channels; and sound control-flow-sensitive security type system for low-level operating system code." Demonstrates on virtual memory, L4 IPC, and AES timing attack countermeasure. CertiKOS: A Certified Kernel for Secure Cloud Computing 2011 Gu et al "Cer- tiKOS isolates guest applications not only from each other but from provider-controlled resource management mechanisms. The ker- nel’s API gives untrusted, provider-supplied management software control over allocation and delegation of resources such as memory and I/O devices, but prohibits management code from accessing a guest’s memory or other resources while in use, or from interfering with a guest’s execution except through clean resource revocation. CertiKOS represents an effort to apply recent advances in certified software design to a ground-up design of a modular and evolvable certified kernel. Through machine-checkable proof certificates and runtime monitoring, CertiKOS aims to offer users the assurance of correct and leak-free execution of their cloud services." CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency 2011 INRIA "We describe ClightTSO, a concurrent extension of CompCert’s Clight in which the TSO-based memory model of x86 multprocessors is exposed for high-performance code, and CompCertTSO, a formally verified compiler from ClightTSO to x86 assembly language, building on CompCert. CompCertTSO is verified in Coq: for any well-behaved and successfully compiled ClightTSO source program, any permitted observable behaviour of the generated assembly code (if it does not run out of memory) is also possible in the source semantics. We also describe some verified fence-elimination optimisations, integrated into CompCertTSO." SCION: Scalability, Control, and Isolation On Next-Generation Networks 2011 Zhang et al. (Networking answer to Clean Slate?) "We present the first Internet architecture designed to provide route control, failure isolation, and explicit trust information for end-to-end communications. SCION separates ASes into groups of independent routing sub-planes, called trust domains, which then interconnect to form complete routes. Trust domains provide natural isolation of routing failures and human misconfiguration, give endpoints strong control for both inbound and outbound traffic, provide meaningful and enforceable trust, and enable scalable routing updates with high path freshness. As a result, our architecture provides strong resilience and security properties as an intrinsic consequence of good design princi- ples, avoiding piecemeal add-on protocols as security patches. Meanwhile, SCION only assumes that a few top-tier ISPs in the trust domain are trusted for providing reliable end-to-end communications, thus achieving a small Trusted Computing Base. Both our security analysis and evaluation results show that SCION naturally prevents numerous attacks and provides a high level of resilience, scalability, control, and isolation." Data-Provenance Verification For Secure Hosts 2012 Xu et al. "We define data- provenance integrity as the security property stating that the source where a piece of data is generated cannot be spoofed or tampered with. We describe a cryptographic provenance verification approach for ensuring system properties and system-data integrity at kernel-level. Its two concrete applications are demonstrated in the keystroke integrity verification and malicious traffic detection. Specifically, we first design and implement an efficient cryptographic protocol that enforces keystroke integrity by utilizing on-chip Trusted Computing Platform (TPM). The protocol prevents the forgery of fake key events by malware under reasonable assumptions. Then, we demonstrate our provenance verification approach by realizing a lightweight framework for restricting outbound malware traffic. This traffic-monitoring framework helps identify network activities of stealthy malware, and lends itself to a powerful personal firewall for examining all outbound traffic of a host that cannot be bypassed." (Note: I love it when they say "cannot be bypassed.") Robust Network Covert Communications Based on TCP and Enumerative Combinatorics 2012 Luo et al "In this paper, we show through a new class of timing channels coined as Cloak that it is possible to devise a 100 percent reliable covert channel and yet offer a much higher data rate (up to an order of magnitude) than the existing timing channels. Cloak is novel in several aspects. First, Cloak uses the different combinations of N packets sent over X flows in each round to represent a message. The combinatorial nature of the encoding methods increases the channel capacity largely with (N; X). Second, based on the well-known 12-fold Way, Cloak offers 10 different encoding and decoding methods, each of which has a unique tradeoff among several important considerations, such as channel capacity and camouflage capability. Third, the packet transmissions modulated by Cloak can be carefully crafted to mimic normal TCP flows for evading detection." Silencing Hardware Backdoors 2011 Waksman & Sethumadhavan "We present the first solution for disabling digital, design- level hardware backdoors. The principle is that rather than try to discover the malicious logic in the design – an extremely hard problem – we make the backdoor design problem itself intractable to the attacker. The key idea is to scramble inputs that are supplied to the hardware units at runtime, making it infeasible for malicious components to acquire the information they need to perform malicious actions. We show that the proposed techniques cover the attack space of deterministic, digital HDL backdoors, provide probabilistic security guarantees, and can be applied to a wide variety of hardware components. Our evaluation with the SPEC 2006 benchmarks shows negligible performance loss (less than 1% on average) and that our techniques can be integrated into contemporary microprocessor designs." Language-Independent Sandboxing of Just-In-Time Compilation and Self-Modifying Code 2011 Ansel & Marchenko Extends SFI to work with JIT and dynamic languages. My first thought was hooking Lua or Stackless python into this. Put that on SeLinux, BSD Capsicum or something. Restricted language subset. That's a hell of a start for a secure enough, but productive, platform. Build everything else in the high level language. Enhancing Data Trustworthiness via Assured Digital Signing 2012 Dai " Specifically, ADS allows a signature verifier to examine not only a signature’s cryptographic validity but also its system security validity that the private signing key and the signing function are secure, despite the powerful attack that the signing application program and the general-purpose Operating System (OS) kernel are malicious. The modular design of ADS makes it application-transparent (i.e., no need to modify the application source code in order to deploy it) and almost hypervisor-independent (i.e., it can be implemented with any Type I hypervisor). To demonstrate the feasibility of ADS, we report the implementation and analysis of an Xen-based ADS system." Nice papers that aren't necessarily new, but I'm including them anyway. Organically assured and survivable information systems 2004 Boeing This was one I started to consider a practical how to on secure service creation. They combine MAC on hosts, an embedded firewall appliance for enforcement/monitoring on every connected device, app hardening techniques, network rate limiting, an effecient byzantine tolerance algorithm, a modified Secure Spread toolkit, and use their A1-class SNS Server as a trust anchor for secure forwarding and other stuff. Talk about putting it all together. Now to make a version of this that companies can use and Boeing doesn't own... ;) Overview of Language-based Security Bibliography (2004) Grossman Good resource for people looking up publications on language-based security up to that point. Includes C-like languages, HLL's, Proof-carrying code, compiler, info-flow security, runtime tools, and many other specialist types of tech. I guess it's also a good resource for beginners to safe/secure language approaches. CODESSEAL - Compiler FPGA approach to secure applications by Gelbaru et al. Join compiler/hardware infrastructure for software protection for fully encrypted execution with both program and data encryptedi n memory. Processor + FPGA-based hardware component for fast crypto, and does code integrity verification, authentication and execution flow protection. HyperSafe: A Lightweight Approach to Provide Lifetime Hypervisor Control-Flow Integrity Wang And Jiang Two techniques to protect control flow integrity of existing hypervisors. They test it with Xen and Bitvisor + synthethic exploits. Secure Embedded Processing through Hardware-assisted Run-time Monitoring 2005 Arora et al. "Specifically, we extract properties of an embedded program through static program analysis, and use them as the bases for enforcing permissible program behavior in real-time as the program executes. We present an architecture for hardware-assisted run-time monitoring, wherein the embedded processor is augmented with a hardware monitor that observes the processor’s dynamic execution trace, checks whether the execution trace falls within the allowed program behavior, and flags any deviations from the expected behavior to trigger appropriate response mechanisms. We present properties that can be used to capture permissibleprogram behavior at different levels of granularity within a program, namely inter-procedural control flow, intra-procedural control flow, and instruction stream integrity. We also present a systematic methodology to design application-specific hardware monitors for any given embedded program. " ChipLock: Support for Secure Microarchitectures 2005 Kgil et al. "We show that security support can be added at some acceptable cost in area and performance. We propose a processor extension called ChipLock. It pro- vides hardware security support for a mostly untrusted operating system to ensure the integrity and confidenti- ality of all computational results. ChipLock’s modular design can be easily integrated into existing hardware platforms with only slight modification to the operating system. ChipLock includes a built-in hardware Key Manager that supports symmetric key assignment, and a read-only-memory, TrustROM, that executes secure hardware routines. " Recovery Oriented Computing - Motivations and Case Studies 2002 Compares different variations of this paradigm. Honestly, the rampant insecurity has made this sound more like a good idea every year. The most basic form IT guys have been doing forever: periodically restore a Windows box to factory condition, install apps, patch it all, and back it up. Maintain backup & periodically restore from it. That's a simple version of ROC. WebDSL: A Case Study in Domain-Specific Language Engineering 2008 Visser It's what it sounds like. Think of Ocsigen, Ur/Web, Opa, Sun's DASL or the typesafe functional web platforms. Combine these ideas with builtin security (a la OWASP security api?) to get what I'm getting at. The Domain-Specific Approach to High Assurance Development ASN.1 Galois Inc. 2006 I was always a fan of ASN.1 over XML. Well, my variants of it anyway. They were simple enough to describe in a page or two, super-easy to parse, and used little bandwidth. Galois takes it to next level with high assurance ASN.1 implementation. SECURING INFORMATION FLOW AT RUNTIME 2009 Shroff "Although static systems for programming language based information flow control are well-studied, few works address runtime security of information flow. Runtime informa- tion flow control offers distinct advantages in precision and in the ability to support dynam- ically defined policies. To this end, this thesis develops dynamic techniques to track direct and indirect flows of information, and secure information leaks due to timing channels, in higher-order programs. We formulate two runtime information flow systems: λdeps and λsync . λdeps secures seq the direct and indirect flows in programs by tracking the dependencies between the values flowing across various program points, while λsync decouples the publicly observable timing seq behavior of programs from secret data by synchronizing the execution times of timing- sensitive pieces of codes. Noninterference results are proved for all our systems." A retrospective on the VAX VMM security kernel 1991 Karger et al. One of the old A1 class products. Good look into rigorous secure system design that accounts for performance, usability and business practicalities. Kemmerer's paper on Shared Resource Matrix and his follow up paper here. They mention the most mature and effective ways of hunting them down. KSOS Looking Back by Tom Perrine in login magazine (just google it) Describes KSOS, one of the old exemplar designs. Compares its features and security to modern stuff. Accuses many modern groups of reinventing the wheel constantly. Commentary on things. Nice read. I also need to do a paper update on secure databases. I have old papers on integrating MLS or A1-class systems with untrusted databases/software for this purpose. Then, there's modern stuff like sharding and type-safe language constructs. I think some of this could be combined in a way that meets security and performance goals with high robustness with moderate cost/effort.