Last February I spent two weeks in Vienna, visiting Jakob Lechner and RUAG Space Austria, a company developing components for space missions. Jakob and his colleagues designed a specialised processing core called REDFIN (REDuced instruction set for Fixed-point & INteger arithmetic) for executing simple spacecraft control tasks, such as satellite antenna pointing. During the visit I implemented a prototype of a formal verification framework to support the development of REDFIN programs. Afterwards I was quite busy with my other projects, but my PhD student Georgy Lukyanov helped to further improve the prototype.
Jakob, Georgy and I have just submitted a conference paper describing the REDFIN core and the verification framework. Please have a look and let us know what you think. This will be a timely read after yesterday’s exciting SpaceX launch.
As we all know, writing programs is easy. Writing correct programs on the other hand is very hard. And if you are writing a program for a space mission you better be sure it is correct. So, what can you realistically do? Of course you should write and/or generate a lot of tests, but tests do not provide the full correctness guarantee. You can also use a strongly typed programming language and prove some properties at compile time, but your space-grade processor is highly unlikely to be a well-supported compilation target (and you might not be able to take your favourite garbage collector to space — it’s way too heavy!). You could also use formal methods and develop programs with the help of a theorem prover, eventually refining an abstract specification down to the level of bare metal. That might take you years though, especially if you have no previous experience in formal methods.
When I was working on my PhD I did some work on formal specification of processors and instruction sets, so this is a long-time interest of mine. Hence, when I heard about the REDFIN project I immediately self-invited myself to RUAG Space Austria and tried to figure out a way to engineer a simple solution that can be integrated into the existing development and verification workflow without a big disruption and a steep learning curve. Eventually I used Haskell to implement a small DSL for capturing the semantics of REDFIN programs and connected it to an SMT solver using SBV, a wonderful symbolic verification library developed by Levent Erkok (huge thanks!). This idea is not new and we reference a few early papers that developed and applied it to Arm and Intel processors. I also got a lot of inspiration from this blog post by Stephen Diehl and this talk by Tikhon Jelvis. Thank you Stephen and Tikhon!
P.S.: The code is not yet available, but I hope we’ll release it soon.