CARET analysis of multithreaded programs

TL;DR

This paper presents a method for model-checking multithreaded programs modeled as Dynamic Pushdown Networks against CARET temporal logic formulas, including programs with lock communication, enabling detection of concurrent malware.

Contribution

It introduces a reduction of CARET model checking for DPNs to B"uchi Dynamic Pushdown Systems, extending decidability to programs with lock communication.

Findings

Model checking DPNs against CARET is decidable.

Reduction to B"uchi Dynamic Pushdown Systems is effective.

Applicable to malware detection in multithreaded programs.

Abstract

Dynamic Pushdown Networks (DPNs) are a natural model for multithreaded programs with (recursive) procedure calls and thread creation. On the other hand, CARET is a temporal logic that allows to write linear temporal formulas while taking into account the matching between calls and returns. We consider in this paper the model-checking problem of DPNs against CARET formulas. We show that this problem can be effectively solved by a reduction to the emptiness problem of B\"uchi Dynamic Pushdown Systems. We then show that CARET model checking is also decidable for DPNs communicating with locks. Our results can, in particular, be used for the detection of concurrent malware.