CertiStr: a certified string solver
Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, M. J. Schrader
Abstract
Theories over strings are among the most heavily researched logical theories in the SMT community in the past decade, owing to the error-prone nature of string manipulations, which often leads to security vulnerabilities (e.g. cross-site scripting and code injection). The majority of the existing decision procedures and solvers for these theories are themselves intricate; they are complicated algorithmically, and also have to deal with a very rich vocabulary of operations. This has led to a plethora of bugs in implementation, which have for instance been discovered through fuzzing.
Topics & Concepts
Computer scienceString (physics)Fuzz testingProgramming languageScripting languageSatisfiability modulo theoriesCross-site scriptingTheoretical computer scienceSuiteCertificationSymbolic executionVocabularySoftware engineeringComputer securityLinguisticsMathematicsSoftwarePolitical scienceWeb application securityMathematical physicsArchaeologyWeb developmentHistoryPhilosophyLawWeb serviceWeb Application Security VulnerabilitiesSecurity and Verification in ComputingSoftware Testing and Debugging Techniques