When it comes to providing software assurance, SPARK, a formally provable subset of Ada, is the best weapon in the arsenal to ensure the absence of data-flow and runtime errors. Furthermore, SPARK offers mechanisms to prove key integrity properties and even complete functional proof of requirements. Regardless of the apparent benefits of using SPARK in safety-critical applications, there is still some reservation in adopting the technology over traditional languages like C and C++, which offer minimum software assurance. Instead, developers in many cases rely on heavy testing approaches with the hope that all the possible bugs will be captured before application deployment. Arguments in favour of such problematic approaches include a perceived steep-learning curve for adopting SPARK, and thus, an increase in production cost, and the assumption that SPARK will significantly negatively impact the execution time of an application. These are all perceptions mainly formed due to a lack of understanding the technology. This paper takes a quantitative approach, where SPARK is put under test, and relevant metrics, such as performance and development time, are recorded to demystify the impact of adopting SPARK and expose any areas that the technology can be further improved. To achieve this a relevant to the industry embedded benchmark suite written in C, the EMBENCH, is converted to Ada and SPARK, to prove the absence of runtime errors, which are well-known sources of security vulnerabilities. Furthermore, we share our valuable experiences on best practices for hardening software libraries using SPARK.
Written by Kyriakos Georgiou, Paul Butcher and Yannick Moy
