Tunable Cyber Defensive Security Mechanisms

Evaluating security mechanisms is a difficult and manual process. To effectively compare different techniques, security analysts use synthetic benchmarks that are typically comprised of simple test cases or a combination of known vulnerabilities in an attempt to provide coverage for different classes of attacks. As such, security mechanisms adapt their techniques to guarantee good coverage for the synthetic benchmarks but provide little guarantees of their efficacy beyond that. To ensure accurate evaluation and comparison of competing security techniques on real-world programs, we need automated techniques for injecting realistic and verifiable vulnerabilities.We propose to develop a new technique and system for automatically generating and injecting realistic vulnerabilities to real-world applications. Our proposed system uses targeted symbolic execution to discover program paths that could be used to generate vulnerabilities (e.g., integer overflows). The programs paths (i.e., symbolic constraints) are then modified using information from formal methods (e.g.,, using SMT solvers) to generate and inject new code , at the source- or binary-level, that is provably vulnerable (e.g., the system can prove that the generated conditions along a specific program path can generate an overflow). If successful, our proposed system can transform the evaluation of security systems and enable novel pedagogical tools.