Specification Inference Modulo Oracles for Database-Backed Web Applications
摘要
In logical reasoning, specification inference attempts to synthesize an explanatory hypothesis from a given conclusion. We consider the specification synthesis problem for database-backed web-applications where only an oracle access to the application is available. Such is a real case for test teams where they are not provided access to the application. Our algorithm begins with an initial hypothesis constructed from responses of the web-application on a sampled dataset, and then improves this hypothesis iteratively via carefully constructed queries to the application (via an SMT solver). Finally, statistical tests are used to validate the soundness and maximality of the constructed hypothesis. We implement our algorithm in a tool, Vivaran, and demonstrate its capabilities on a large web-based enterprise resource planning (ERP) software. Vivaran infers semantically equivalent specifications as the ground-truth in all cases.