Un Método de Verificación Formal de Compilación Basado en un Subconjunto Seguro de C

Con el rápido aumento en el número de terminales inalámbricos y la apertura de las redes inalámbricas, la seguridad de la comunicación inalámbrica está enfrentando desafíos serios. La seguridad de la comunicación informática siempre ha sido un tema de investigación importante, especialmente la comunicación inalámbrica que aún tiene una arquitectura más compleja que conlleva a más problemas de seguridad en el desarrollo del sistema de comunicación. En los últimos años, cada vez más sistemas de comunicación inalámbrica se aplican en el campo crítico de seguridad que tiende a necesitar garantías de alta seguridad. Un compilador es una herramienta importante para el desarrollo del sistema, y su seguridad y confiabilidad tienen un impacto importante en el desarrollo de software crítico de seguridad. Como el método más estricto, los métodos de verificación formal han sido ampliamente atendidos en la verificación de compiladores, pero los métodos actuales de verificación formal tienen algunos problemas, como alta complejidad de prueba, débil capacidad de verificación y baja eficiencia del algoritmo. En este documento, se

Autores: Tan, Yu; Ma, Dianfu; Qiao, Lei