june 2013 update of security papers

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 eect 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.