Las propiedades intelectuales de hardware (IP) de proveedores no confiables son ampliamente utilizadas, lo que plantea preocupaciones de seguridad para los diseñadores de sistemas. Aunque los métodos formales proporcionan soluciones poderosas para detectar comportamientos maliciosos en hardware, la participación del trabajo manual impide que los métodos alcancen aplicaciones prácticas. Por ejemplo, el Seguimiento de Flujo de Información (IFT) representa un enfoque poderoso para prevenir la fuga de información sensible. Sin embargo, las soluciones de IFT existentes introducen sobrecargas de hardware o carecen de procedimientos de trabajo automático prácticos, especialmente para la lógica secuencial de hardware. Para aliviar estos desafíos, proponemos un marco que automatiza completamente la detección de fugas de información a nivel de compuerta de hardware. Este marco introduce Z3, un solucionador SMT, para verificar automáticamente la violación de la confidencialidad. Por otro lado, se desarrolla una herramienta automática para eliminar aún más la carga de trabajo manual. En esta herramienta, el hardware a nivel de compuerta se convierte primero en el modelo formal, y se evalúa la integridad del modelo. Junto con el paso de conversión del modelo, también se genera la propiedad para la detección de fugas. La solución propuesta se prueba en 25 bancos de pruebas de netlist a nivel de compuerta, donde se incluyen diseños secuenciales para validar la efectividad. Como resultado, los troyanos que filtran información desde las salidas del circuito pueden ser detectados automáticamente. El tiempo de consumo medido de todo el procedimiento de trabajo valida la eficiencia del enfoque propuesto.