A Trustworthy Translation Method for Synchronous Data Flow Language that Eliminates Implicit Type Conversions

This paper addresses the security vulnerabilities present in current translation tools for synchronous data flow languages and proposes a trustworthy translation method designed to eliminate implicit type conversions. First, the paper identifies and analyzes limitations in existing tools, particularly regarding secure coding standards. An enhanced translation algorithm is then developed using the Coq theorem prover, which modifies the Ctemp abstract syntax tree to eliminate implicit type conversions in the generated code. Subsequently, formal verification is applied to the translation functions to establish the correctness of the translation process. Finally, the implementation of a trusted translation tool for synchronous data flow languages is completed and tested rigorously. Experimental results demonstrate that this approach effectively eliminates implicit types in the generated code, significantly improving code security. This work integrates secure coding standards with synchronous data flow language translation, offering new approaches and methodologies for trusted compilation in the synchronous data flow language domain.