The current version of the PCM-based analysis does not follow to original specification from here. Violations of confidentiality requirements are found one data flow diagram node, i.e., one entry in the action sequence to early, i.e., in node n - 1. This becomes visible when comparing the PCM-based analysis with the vanilla DFD analysis.

The original specification states: "The label comparison function compares the classification label of incoming data with the clearance label of the receiving node." (p. 97). This can happen because we do not generate an exit node for SEFFs, so the check happens "implicitly" on the out pin of the node n - 1.

TL;DR, we propose two changes:

• Add the generation of SEFF exit nodes, see p. 174
• The constraint should be evaluated on the state of the input pin, not the output pin