Sliver: A Scalable Slicing-Based Verification for Information Flow Security

Static information flow analysis has been studied for a long time. It is usually considered more precise than dynamic taint analysis and more flexible and indispensable when running individual modules or the entire program is difficult. The state-of-the-art static information flow analyses are scalable on analyzing Java programs or mobile apps, and several type systems have enforced information flow security on different languages. However, static information-flow analyses have rarely scaled up to real-world C programs. This work presents Sliver, a slicing-based approach to verify information flow security on real-world C programs. The principle of Sliver is to convert the information-flow-involved parts of the original program into behavior-equivalent slices and use bounded model checking to enforce the end-to-end noninterference property or detect security violations on the slices after self-composition. We develop automated path-signature-guided slicing and adaptive self-composition approaches to ensure Sliver's efficacy and scalability. We also develop a consistency testing technique and metrics to estimate the correctness of slices generated by Sliver. The evaluations demonstrate Sliver's effectiveness, scalability, and the correctness of the generated slices.