Rfblare (Race-Free Blare) is a new version of KBlare, developped for the kernel version 4.7 and onwards. It is designed to overcome two major problems impacting information flow trackers built on the Linux Security Modules framework (including KBlare).
Rfblare solves both of this problem using a new tags propagation algorithm.
Rfblare is still a young project, and while it is built upon the knowledge acquired by the design and implementation of Kblare, it is not complete yet. For now, there is no notion of policy in Rfblare. Only the tags propagation mechanism is implemented.
See the Rfblare guides for details about installing and testing Rfblare, as well as a description of some attacks on LSM-based trackers Rfblare can counter.
The proofs of the formal results in the article describing Rfblare accepted at SEFM 2017 can be downloaded here. They have been formally verified with Coq, the proof assistant, version 8.6. The file can be viewed in a browser here or downloaded here.
You can also consult the Kblare page for details about KBlare.