Team Edit Automata for Testing Security Property

This paper introduces a mathematical model, called team edit automata, for evaluating software security properties. We use the model to describe security properties and their correlation in the software programs. The component automata can suppress and insert actions and report possible flaws. They are used to specify individual security properties. The team is composed of multiple component automata interacting through shared actions. It models the situation where some program events are concerned by multiple security properties jointly. The paper concludes by a case study of detecting memory management and pointer manipulation flaws in C/C++ programs.