Branching Temporal Logic of Calls and Returns for Pushdown Systems

TL;DR

This paper introduces BCARET, a branching temporal logic for pushdown systems that accounts for call-return matching, with effective model-checking methods applicable to malware detection.

Contribution

It defines BCARET logic for PDSs, providing a reduction-based model-checking approach for both standard and regular valuations.

Findings

Model-checking problems are reducible to emptiness problems of Alternating Büchi Pushdown Systems.

Effective algorithms are provided for verifying PDSs against BCARET formulas.

Applications include malware detection using the proposed logic and methods.

Abstract

Pushdown Systems (PDSs) are a natural model for sequential programs with (recursive) procedure calls. In this work, we define the Branching temporal logic of CAlls and RETurns (BCARET) that allows to write branching temporal formulas while taking into account the matching between calls and returns. We consider the model-checking problem of PDSs against BCARET formulas with "standard" valuations (where an atomic proposition holds at a configuration c or not depends only on the control state of c, not on its stack) as well as regular valuations (where the set of configurations in which an atomic proposition holds is regular). We show that these problems can be effectively solved by a reduction to the emptiness problem of Alternating B\"uchi Pushdown Systems. We show that our results can be applied for malware detection.