Securing Antiquated Languages via program Synthesis and human Assistance (SALSA)

We will continue to develop our Phase I translation software for converting legacy C code into Go, building mature software that is practicable and theoretically sound. To demonstrate the maturity of our translation software, we will translate the COBOL compiler GnuCOBOL from C to Go. At a very high level, our Phase II efforts will consist of technical improvements to our lifting tools for program synthesis, along with a new suite of tools for making the translation process more efficient, more robust, and less reliant on user input. Our Phase I efforts were organized around a synthesis engine coded in Rosette, which enables Rosette to view Go code as being punctured periodically with holes, where the holes refer to various patterns of unsafe behavior produced by a baseline “naive” translation from C to Go. The Rosette synthesis engine then uses an SMT solver to fill those holes, replacing the pattern of unsafe behavior with a pattern of safe behavior. Additionally, in Phase I we built a Go utilities library that managed the parsing and translation of Go code into abstract syntax trees into S-expressions and back, to bridge between the raw C code and the finished Go code. Our Phase II efforts will consist of continuing the development of our Phase I synthesis engine, along with improving the automation of the code to reduce the need for human-in-the-loop elements, and improving the verifiability of the translation by automatically generating a large family of test cases. For the Phase I synthesis engine, the areas where our Phase I translation software needs to be especially improved are in handling heap-allocated data and in parsing side-effecting functions. One interesting technical challenge to translating GnuCOBOL from C to Go is that significant portions of GnuCOBOL are written in Yacc (Yet another compiler-compiler), a parser generator. Lifting Yacc to Go will require new tools for identifying ambiguous grammars and lifting Yacc parsers to Go parsers. However, once complete, the translation will serve both as a demonstration of our SALSA translation tools, and as a platform that could lead to future work on translating COBOL.