Taxonomic Search: david OR melski, Presentation
Results 1 - 10 of 27
Results
file
586.26 KB- 0 views
- 160 downloads
- Download
file
ABSTRACT
Cyber-physical systems (CPS) are becoming an increasingly attractive target for adversaries to launch software attacks against. New approaches are needed to detect software-based vulnerabilities while meeting the constraints of embedded execution in CPS.
file
The verification architecture of the Guardol system uses an implementation of HOL (Higher Order Logic) as a front end to SMT (Satisfiability Modulo Theories) technology. SMT provides high levels of proof automation. HOL provides semantic power, modelling the operational semantics of Guardol, an imperative language, and justifying the automatic deductive translation of programs to the functional form needed by SMT technology. In the Guardol system, extensive manipulation of programs and specifications is performed in HOL before goals are sent to the backend RADA SMT system.
file
Charles Farrar, "New Cyber-Physical Systems Education Activities at Los Alamos National Laboratory." Invited talk at the First Workshop on Cyber-Physical Systems Education (CPS-Ed 2013) at Cyber Physical Systems Week (CPSWeek 2013), Philadelphia, Pennsylvania, USA, April 2013.
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.
