- Bidirectional Grammars for Machine-Code Decoding and Encoding. G. Tan and G. Morrisett.
In 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2016.
[paper]
Abstract: Binary analysis, which analyzes machine code, requires a decoder for converting bits into abstract syntax of machine instructions. Binary rewriting requires an encoder for converting instructions to bits. We propose a domain-specific language that enables the specification of both decoding and encoding in a single bidirectional grammar. With dependent types, a bigrammar enables the extraction of an executable decoder and encoder as well as a correctness proof showing their consistency. The bigrammar DSL is embedded in Coq with machine-checked proofs. We have used the bigrammar DSL to specify the decoding and encoding of a subset of x86-32 that includes around 300 instructions.
- NativeGuard: Protecting Android Applications from Third-Party Native Libraries. . M. Sun and G. Tan. In 7th ACM Conference on Security and Privacy in Wireless and Mobile Networks (WiSec '14), 2014.
[paper]
Abstract: Android applications often include third-party libraries writ- ten in native code. However, current native components are not well managed by Android.s security architecture. We present NativeGuard, a security framework that isolates native libraries from other components in Android applica- tions. Leveraging the process-based protection in Android, NativeGuard isolates native libraries of an Android applica- tion into a second application where unnecessary privileges are eliminated. NativeGuard requires neither modifications to Android nor access to the source code of an application. It addresses multiple technical issues to support various in- terfaces that Android provides to the native world. Exper- imental results demonstrate that our framework works well with a set of real-world applications, and incurs only modest overhead on benchmark programs.
- Bringing Java's Wild Native World under Control.. M. Sun, G. Tan, J. Siefers, B. Zeng, and G. Morrisett. In ACM Transactions on Information and System Security (TISSEC). Nov. 2013.
[paper]
Abstract: For performance and for incorporating legacy libraries, many Java applications contain native-code components written in unsafe languages such as C and C++. Native-code components interoperate with Java components through the Java Native Interface (JNI). As native code is not regulated by Java.s security model, it poses serious security threats to the managed Java world. We introduce a security framework that extends Java.s security model and brings native code under control. Leveraging software-based fault isolation, the framework puts native code in a separate sandbox and allows the interaction between the native world and the Java world only through a carefully designed pathway. Two different implementations were built. In one implementation, the security framework is integrated into a Java Virtual Machine (JVM). In the second implementation, the framework is built outside of the JVM and takes advantage of JVM-independent interfaces. The second implementation provides JVM portability, at the expense of some performance degradation. Evaluation of our framework demonstrates that it incurs modest runtime overhead while significantly enhancing the security of Java applications.
- Strato: A Retargetable Framework for Low-Level Inlined-Reference Monitors. B. Zeng, G. Tan, and U. Erlingsson. In 22nd Usenix Security Symposium, 2013.
[paper]
Abstract: Low-level Inlined Reference Monitors (IRM) such as control-flow integrity and software-based fault isolation can foil numerous software attacks. Conventionally, those IRMs are implemented through binary rewriting or transformation on equivalent low-level programs that are tightly coupled with a specific Instruction Set Architecture (ISA). Resulting implementations have poor retargetability to different ISAs. This paper introduces an IRM-implementation framework at a compiler intermediate-representation (IR) level. The IR-level framework enables easy retargetability to different ISAs, but raises the challenge of how to preserve security at the low level, as the compiler backend might invalidate the assumptions at the IR level. We propose a constraint language to encode the assumptions and check whether they still hold after the backend transformations and optimizations. Furthermore, an independent verifier is implemented to validate the security of low-level code. We have implemented the framework inside LLVM to enforce the policy of control-flow integrity and data sandboxing for both reads and writes. Experimental results d\ emonstrate that it incurs modest runtime overhead of 19.90% and 25.34% on SPECint2000 programs for x86-32 and x86-64, respectively.
- JVM-Portable Sandboxing of Java's Native Libraries. M. Sun and G. Tan. In European Symposium on Research in Computer Security (ESORICS '12).
[paper]
Abstract: Although Java provides strong support for safety and security, native libraries used in a Java application can open security holes. Previous work, Robusta, puts native libraries in a sandbox to protect the integrity and security of Java. However, Robusta's implementation modies the internals of OpenJDK, a particular implementation of a Java Virtual Machine (JVM). As such, it is not portable to other JVM implementations. This paper shows how to make the idea of sandboxing native libraries JVM-portable. We present a two-layer approach for sandboxing without modifying the internals of a JVM. We also discuss our experience of sandboxing Java's core native libraries. Experiments show that our approach of JVM-portable sandboxing incurs modest performance overhead on SPECjvm 2008 benchmark programs.
- RockSalt: Better, Faster, Stronger SFI for the x86. G. Morrisett, G. Tan, J. Tassarotti, J.B. Tristan, and E. Gan.
In ACM Conference on Programming Language Design and Implementation (PLDI '2012).
[paper]
Abstract: Software-based fault isolation (SFI), as used in Google.s Native Client (NaCl), relies upon a conceptually simple machine-code analysis to enforce a security policy. But for complicated architectures such as the x86, it is all too easy to get the details of the analysis wrong. We have built a new checker that is smaller, faster, and has a much reduced trusted computing base when compared to Google.s original analysis. The key to our approach is automatically generating the bulk of the analysis from a declarative description which we relate to a formal model of a subset of the x86 instruction set architecture. The x86 model, developed in Coq, is of independent interest and should be usable for a wide range of machine-level veri.cation tasks.
- Combining Control-Flow Integrity and Static Analysis for Efficient and Validated Data Sandboxing. B. Zeng, G. Tan, and G. Morrisett.
In the 18th ACM Conference on Computer and Communication Security (CCS '11)
[paper]
Abstract: In many software attacks, inducing an illegal control-flow transfer in the target system is one common step. Control-Flow Integrity (CFI) protects a software system by enforcing a pre-determined control-flow graph. In addition to providing strong security, CFI enables static analysis on low-level code. %thanks to its guaranteed static control-flow graph. This paper evaluates whether CFI-enabled static analysis can help build efficient and validated data sandboxing. Previous systems generally sandbox memory writes for integrity, but avoid protecting confidentiality due to the high overhead of sandboxing memory reads. To reduce overhead, we have implemented a series of optimizations that remove sandboxing instructions if they are proven unnecessary by static analysis. On top of CFI, our system adds only 2.7% runtime overhead on SPECint2000 for sandboxing memory writes and adds modest 19% for sandboxing both reads and writes. We have also built a principled data-sandboxing verifier based on range analysis. The verifier checks the safety of the results of the optimizer, which removes the need to trust the rewriter and optimizer. Our results show that the combination of CFI and static analysis has the potential of bringing down the cost of general inlined reference monitors, while maintaining strong security.
- JNI Light: An Operational Model for the Core JNI. G. Tan. In the 8th Asian Symposium on Programming Languages and Systems (APLAS '10)
[paper
|tech report]
Abstract: Through foreign function interfaces (FFIs), software components in different programming languages interact with each other in the same address space. Recent years have witnessed a number of systems that analyze FFIs for safety and reliability. However, lack of formal specifications of FFIs hampers progress in this endeavor. We present a formal operational model, JNI Light (JNIL), for a subset of a widely used FFI---the Java Native Interface (JNI). JNIL focuses on the core issues when a high-level garbage-collected language interacts with a low-level language. It proposes abstractions for handling a shared heap, cross-language method calls, cross-language exception handling, and garbage collection. JNIL can directly serve as a formal basis for JNI tools and systems. The abstractions in JNIL are also useful when modeling other FFIs, such as the Python/C interface and the OCaml/C interface.
- Weak updates and separation logic. G. Tan, Z. Shao, X. Feng and H. Cai. In the Journal of New Generation Computing.
[paper]
Abstract: Separation logic provides a simple but powerful technique for reasoning about low-level imperative programs that use shared data structures. Unfortunately, separation logic supports only ``strong updates'', in which mutation to a heap location is safe only if a unique reference is owned. This limits the applicability of separation logic when reasoning about the interaction between many high-level languages (e.g., ML, Java, C#) and low-level ones since the high-level languages do not support strong updates. Instead, they adopt the discipline of ``weak updates'', in which there is a global ``heap type'' to enforce the invariant of type-preserving heap updates. We present SL^w, a logic that extends separation logic with reference types and elegantly reasons about the interaction between strong and weak updates. We describe a semantic framework for reference types, which is used to prove the soundness of SL^w. Finally, we show how to extend SL^w with concurrency.
- Robusta: Taming the Native Beast of the JVM. J. Siefers, G. Tan, and G. Morrisett. In the 17th ACM Conference on Computer and Communication Security (CCS '10), Oct. 2010.
[paper]
Abstract: Java applications often need to incorporate native-code components for efficiency and for reusing legacy code. However, it is well known that the use of native code defeats Java's security model. We describe the design and implementation of Robusta, a complete framework that provides safety and security to native code in Java applications. Starting from software-based fault isolation (SFI), Robusta isolates native code into a sandbox where dynamic linking/loading of libraries is supported and unsafe system modification and confidentiality violations are prevented. It also mediates native system calls according to a security policy by connecting to Java's security manager. Our prototype implementation of Robusta is based on Native Client and OpenJDK. Experiments in this prototype demonstrate Robusta is effective and efficient, with modest runtime overhead on a set of JNI benchmark programs. Robusta can be used to sandbox native libraries used in Java's system classes to prevent attackers from exploiting bugs in the libraries. It can also enable trustworthy execution of mobile Java programs with native libraries. The design of Robusta should also be applicable when other type-safe languages (e.g., C#, Python) want to ensure safe interoperation with native libraries.
- Weak updates and separation logic. G. Tan, Z. Shao, X. Feng and H. Cai. In the 7th Asian Symposium on Programming Languages and Systems (APLAS '09), Dec. 2009. [paper |tech report] (note: superseded by the journal version above)