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.
| Identifer | oai:union.ndltd.org:UPSALLA1/oai:DiVA.org:kth-332124 |
| Date | January 2023 |
| Creators | Maiga, Aïssata |
| Publisher | KTH, Skolan för elektroteknik och datavetenskap (EECS), Stockholm : KTH Royal Institute of Technology |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | Swedish |
| Type | Student thesis, info:eu-repo/semantics/bachelorThesis, text |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | TRITA-EECS-EX ; 2023:496 |
Page generated in 0.0023 seconds