Execution Trace Analysis Using LTL FO
We explore of use of the tool BeepBeep, a monitor for the temporal logic LTL FO\ in interpreting assembly traces, focusing on security related applications. LTL FO\ is an extension of LTL, which includes first order quantification. We show that LTL FO\ is a sufficiently expressive formalism to state a number of interesting program behaviors, and demonstrate experimentally that BeepBeep can efficiently verify the validity of the properties on assembly traces in tractable time.
ISoLA