« Back to main Programme

Programming Languages for C-cured Software

Yannick Moy

SPARK Product Manager and Research Directions Lead, AdaCore

The recent years have seen a renewed interest in the choice of programming language in the development of important/critical software. There is increased realization that some programming languages come with pitfalls that impact the quality of the software produced in that language, with direct consequences for safety and security. This was the main message of the presentation by ANSSI on "Mind your language(s), A Discussion about Languages and Security" at HIS 2014. This is now a mainstream topic of discussion. Looking beyond mere pitfalls, some programming languages contain at their core a few "defect attractors", a term coined by Les Hatton and popularized by Eric Raymond, which defeat attempts at higher software quality. C is a hugely popular programming language for developing important/critical software, in particular embedded software, that has a high number of defect attractors: pointer arithmetic, type punning, manual memory management, text-substitution macros, global variables, manual error handling, implicit type conversions, minimality of syntax. In this presentation, we will discuss major defect attractors in mainstream programming languages such as C/C++, and how they are avoided in well established programming lanugages (such as Ada/OCaml), more recent programming languages (such as Rust/Go), new versions of programming languages (such as C++17/C++20) or subsets of programming languages (such as MISRA-C/SPARK Ada). We will highlight whether the defense comes from language constructs, supporting tools, or a combination thereof.

About Yannick Moy

Yannick Moy is Product Manager for the AdaCore SPARK toolsuite, and lead of the Research Directions team at AdaCore. Yannick Moy’s work focuses on software source code analysis for defect detection and formal verification of safety/security properties. He has presented AdaCore's work around SPARK in numerous articles, conferences, classes and blogs (in particular blog.adacore.com). Prior to joining AdaCore, Yannick led the development of the C++ Verifier for Polyspace (now part of MathWorks). Thereafter Yannick worked at Inria Research Labs/Orange Labs in France to carry out a PhD on automatic modular static safety checking for C programs. Yannick joined AdaCore in 2009, after a short internship at Microsoft Research. Yannick holds an engineering degree from the Ecole Polytechnique, an MSc from Stanford University and a PhD from Université Paris-Sud. He is a Siebel Scholar.

Sponsored by

AdaCore Altran Jaguar Land Rover

Supported by

BAE Systems