Abstract: Due to the incompleteness of the "Unwinding Theorem",a system can't be judged to fail to satisfy the forward correctability, when some local conditions of "Unwinding Theorem" are not satisfied. This paper proposed an algorithmic verification technique to check the forward correctability based on the state transition system. The technique reduces forward correctability checking to the reachability problem and the reduction enables us to use the reachability checking technique to perform forward correctability checking. Our method is complete and it can give a counter-examples to control and eliminate the illegal information flow when a system fails to satisfy the forward correctability. Finally,Disk-arm Convert Channel illustrates the effectiveness and practicality.

Key words: Forward correctability,Information flow, Non-interference, Sate transition system