Vertx: Automated Validation of Binary Transformations

The paper describes Vertx, a tool for validating software binary transformations. Vertx enables software developers and system administrators to automatically check the correctness of software binary transformations such as security hardening and optimization. Transformation validation increases user trust in binary-transformation technology and allows binary transformations to be safely used in critical applications that have narrow margins of error.