SECloud: Binary Analyzing Using Symbolic Execution in the Cloud

SECloud is a automatic platform to deal with the resource-intensive and labor-intensive nature of high-quality software analysis. SECloud parallelizes symbolic execution in computing cloud to cope with path explosion. To our knowledge, SECloud is the first binary analyzing software that scales to large clusters of machines and can automatically test real-world softwares (e.g., Squirrel, Aeon, Socat, Aspell, Atphttpd) effectively. It utilizes the technology of loop elision and state merging to reduce the executing path state explosion. SECloud can also diagnose incomplete software patches by analyzing the difference pathes caused by patches. SECloud offers a flexible testing service according to the software testing task. It runs on computing clouds, like Amazon EC2, and takes advantage of the the flexible computing resource of cloud. Our experiment results show that SECloud can achive 3 to 4 orders of magnitude speedup comparing a state-of-the-art symbolic execution engine (e.g., S2E).