Taxonomic Search: Academia
Results 1 - 10 of 748
Results
file
ABSTRACT
Verification of binary programs is required to assure their correct execution. However, correctness verification of binary programs often involves significant user expertise and time-consuming manual effort. We present an approach for automatically verifying some x86 binary programs using symbolic execution on a formal model of the x86 instruction set architecture. Our approach can reduce the work involved in the proof development process by automating the verification of program fragments and sometimes even complete subroutines.
file
ABSTRACT
Multiprocessors are now so widespread that verification cannot ignore any longer the flavor of concurrency that they implement. Contrary to what most formal verification works assume, the execution model for concurrent programs is not Lamport's Sequential Consistency (SC), where an execution of a program corresponds to an interleaving of the instructions of the program.
file
ABSTRACT
In recent years, we have seen a proliferation of small, embedded, electronic devices controlled by computer processors as powerful as the ARM®. These devices are now responsible for tasks as varied as flying a plane, talking on a cellphone, or helping to perform surgery. Some of these tasks have severe consequences for a mistake caused by faulty programming or missed deadlines. The best defense against these mistakes is to prevent them from happening in the first place.
file
ABSTRACT
Native Client (NaCL) is a new service provided by Google's Chrome for directly executing native binary code in the context of the browser. The security of NaCL depends upon a binary checker that is meant to enforce a basic sandbox policy known as software-based fault isolation. Recently, we built a new binary checker for NaCL and verified its correctness using the Coq proof assistant: If the checker says "yes" on a binary, and the binary is loaded into a suitable context, then the binary is guaranteed to respect the sandbox.
file
ABSTRACT
Over the last decade, SMT solvers [1, 2] have made a huge impact in automatic bug-finding, analysis and verification of desktop software. More recently, string solvers are starting to have a similar impact on security analysis and vulnerability detection in web applications. String solvers provide a rich constraint language essential for security analysis of web applications, and recently have become efficient enough to be used at scale.
file
ABSTRACT
JavaScript provides access to all resources via object properties. An access control mechanism that protects confidential information for such a language has to gauge traversals of the object graph. We propose a domain specific language to specify sets of objects, assign read and write permissions to them, and enforce these permissions in limited scopes of a program. To obtain complete interposition, we build the enforcement mechanism into the scripting engine.
