SecVerifier: A Practical Memory-Security Verifier

Memory-related security vulnerabilities such as buffer overflow may cause severe consequences once exploited. Various technologies have been applied to discover them before a product is released, but they have significant false positives and false negatives. Formal verification has the reputation of mathematically reasoning about software properties, but it has limited scalability and is challenging to use. We have developed the novel manageable verification unit strategy to address the scalability issue and built a web-based verification service to lower the usage obstacles. With the system, we have verified 140K+ lines of real-world products and discovered 106 memory-related vulnerabilities that other technologies have missed.