Programmers compose programs in multiple languages to combine the advantages of innovations in new high-level programming languages with decades of engineering effort in legacy libraries and systems. For language inter-operation, language designers provide two classes of multilingual programming interfaces: (1) foreign function interfaces and (2) code generation interfaces. These interfaces embody the semantic mismatch for developers and multilingual systems builders. Their programming rules are difficult or impossible to verify. As a direct consequence, multilingual programs are full of bugs at interface boundaries, and debuggers cannot assist developers across these lines. This dissertation shows how to use composition of single language systems and interposition to improve the safety of multilingual programs. Our compositional approach is scalable by construction because it does not require any changes to single-language systems, and it leverages their engineering efforts. We show it is effective by composing a variety of multilingual tools that help programmers eliminate bugs. We present the first concise taxonomy and formal description of multilingual programming interfaces and their programming rules. We next compose three classes of multilingual tools: (1) Dynamic bug checkers for foreign function interfaces. We demonstrate a new approach for automatically generating a dynamic bug checker by interposing on foreign function interfaces, and we show that it finds bugs in real-world applications including Eclipse, Subversion, and Java Gnome. (2) Multilingual debuggers for foreign function interfaces. We introduce an intermediate agent that wraps all the methods and functions at language boundaries. This intermediate agent is sufficient to build all the essential debugging features used in single-language debuggers. (3) Safe macros for code generation interfaces. We design a safe macro language, called Marco, that generates programs in any language and demonstrate it by implementing checkers for SQL and C++ generators. To check the correctness of the generated programs, Marco queries single-language compilers and interpreters through code generation interfaces. Using their error messages, Marco points out the errors in program generators. In summary, this dissertation presents the first concise taxonomy and formal specification of multilingual interfaces and, based on this taxonomy, shows how to compose multilingual tools to improve safety in multilingual programs. Our results show that our compositional approach is scalable and effective for improving safety in real-world multilingual programs. / text

This thesis aims to provide recommendations for interfacing two memory-safe programming languages, Rust and SPARK. The comparison of Rust and C/C++, as well as SPARK and C/C++, has been thoroughly researched. However, this level of investigation hasn’t been as extensive between memory-safe languages. SPARK is a subset of Ada, a programming language with a long track record in safety-critical applications. Rust is a multi-paradigm language that has gained popularity since its emergence roughly a decade ago. Both languages implement ownership systems and type safety, which are instrumental in developing safe and reliable software. Memory-safety bugs in code written in C/C++ account for about 70 % of major vulnerabilities in the industry, as reported by organizations such as Microsoft, Apple, and Google. While tools to avoid memory errors exist, code cannot be made safe retroactively, which creates a need for languages designed with safety in mind, such as Rust and SPARK. Combining those two languages is a very promising path for low-level and systems programming and safety-critical applications (automotive, avionics, medical etc.). This thesis identifies best practices for safe bindings between Rust and SPARK, focusing on ensuring memory safety, type safety, and ownership, and then analyzes how to maintain or transfer those properties. The thesis provides clear recommendations based on control study programs and a real-world example using BBQueue, a circular buffer library suitable for embedded systems implemented in both languages. The identified best practices can be used for safe bindings and automated tools/code generation. This thesis fills a gap in existing research, primarily focusing on combining safe and unsafe languages. It provides a valuable contribution to software security and safety-critical systems. / Denna avhandling syftar till att ge rekommendationer för att koppla samman två minnessäkra programmeringsspråk, Rust och SPARK. Sådana kombinationer har redan studerats utförligt mellan Rust/SPARK och de osäkra språken C/C++, men det finns relativt lite information och forskning angående minnessäkra språk. SPARK är en delmängd av Ada, ett språk som har använts i decenier i säkerhetskritiska applikationer. Rust är ett multiparadigmatiskt språk som har blivit populärt sedan dess skapande för ungefär ett decennium sedan. Båda språken implementerar ägarskapssystem och typsäkerhet, vilka är avgörande för att utveckla säkra och tillförlitliga programvaror. Minnesfel i C/C++ står för cirka 70 procent av de stora sårbarheterna i branschen, som rapporterats av organisationer såsom Microsoft, Apple och Google. Även om det finns verktyg för att undvika minnesfel kan koden inte göras säker retroaktivt, vilket skapar ett behov av språk som är designade med säkerhet i åtanke. Att kombinera Rust och SPARK är en mycket lovande väg för systemprogrammering, låg nivå och säkerhetskritiska applikationer (bilindustri, flygavionik, medicinskt etc). Denna avhandling identifierar bästa praxis för säkra bindningar mellan Rust och SPARK, med fokus på att säkerställa minnessäkerhet, typsäkerhet och ägarskap, och analyserar sedan hur man kan behålla eller överföra dessa egenskaper. Avhandlingen ger klara rekommendationer baserade på kontrollstudieprogram och ett exempel med hjälp av BBQueue, ett cirkulärt buffertbibliotek som används i inbyggda system. Dessa resulat kan användas för att skapa säkra bindningar, manuelt eller med ett automatiserat verktyg. Denna avhandling fyller en lucka i befintlig forskning, som främst fokuserar på att kombinera säkra och osäkra språk. Den bidrar värdefullt till programvarusäkerhet och säkerhetskritiska system.