Dynamically adjusting the security label of each subject is a main approach to improving the availability of MAC models. It includes the method of security label range and the method of taint propagation. The former lacks the support for a less proviledge subject, and the latter has a known covert channels. In this paper, a model called generalized taint propagation model (GTPM) is proposed to protect the confidentiality and integrity of operating systems. It inherits the least privilege characteristic of taint propagation model (TPM), expands the semantics of TPM to close the known covert channels, and introduces declassification and decontamination capacities of subjects to avoid accumulating contamination. The paper also introduces its specification using communicating sequential processes (CSP) language to clear the formal semantics of a GTPM operating system's behaviors of information flow control; Moreover, the study noninterference with declassification in CSP verification model of process equivalence, and proves that abstract GTPM system have the security property of noninterference with declassification in virtue of FDR tool. Finally, this paper uses an example to demonstrate its improvement of availability.