A security type checker for the P4 programming language, TAP4S employs lightweight interval analysis combined with security labels to guarantee the noninterference of P4 programs, providing both soundness guarantees and practical permissiveness.

A prototype tool that relies on type-based dependency analysis and symbolic tuples to disjunctively track dependencies across different program execution paths and verify them against the disjunctive security policy of the underlying database.

DynCoVer is a prototype tool for verifying program security under dynamic policies. It uses symbolic execution and the Z3 solver to symbolically execute Java programs and check their security against the active policy at each observable output.

Je is a programming language model for developing secure enclave applications. It uses high-level abstractions to partition Java programs into enclave and non-enclave components, along with a security type system to guarantee the robustness of the enclave part.