Página 1 dos resultados de 2 itens digitais encontrados em 0.006 segundos
Combining Control-Flow Integrity and Static Analysis for Efficient and Validated Data Sandboxing
Fonte: Association for Computing Machinery
Publicador: Association for Computing Machinery
Tipo: Monograph or Book
EN_US
Relevância na Pesquisa
66.63%
#security#verification#control-flow integrity#static analysis#binary rewriting#inlined reference monitors
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. 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.; Engineering and Applied Sciences
Link permanente para citações:
A Proof Carrying Code Framework for Inlined Reference Monitors in Java Bytecode
Fonte: Universidade Cornell
Publicador: Universidade Cornell
Tipo: Artigo de Revista Científica
Publicado em 14/12/2010
Relevância na Pesquisa
46.4%
We propose a light-weight approach for certification of monitor inlining for
sequential Java bytecode using proof-carrying code. The goal is to enable the
use of monitoring for quality assurance at development time, while minimizing
the need for post-shipping code rewrites as well as changes to the end-host
TCB. Standard automaton-based security policies express constraints on allowed
API call/return sequences. Proofs are represented as JML-style program
annotations. This is adequate in our case as all proofs generated in our
framework are recognized in time polynomial in the size of the program. Policy
adherence is proved by comparing the transitions of an inlined monitor with
those of a trusted "ghost" monitor represented using JML-style annotations. At
time of receiving a program with proof annotations, it is sufficient for the
receiver to plug in its own trusted ghost monitor and check the resulting
verification conditions, to verify that inlining has been performed correctly,
of the correct policy. We have proved correctness of the approach at the Java
bytecode level and formalized the proof of soundness in Coq. An implementation,
including an application loader running on a mobile device, is available, and
we conclude by giving benchmarks for two sample applications.
Link permanente para citações: