The gist of discussion on my earlier blog on the “Relative Security of the ARM vs. x86 architectures” can be summarized in two bullets.
1. It is interesting that at least theoretically, a proper Harvard Architecture based chip might provide a better foundation for building a secure control system than a von Neumann based chip architecture.
2. Other factors, e.g. understanding (understanding the technologies that each processor gives, like the non-executable bits, the different kind of memory access that they can put in their product, etc), talent availability (affordable people with the understanding required to code to the chip correctly) and various derivative operating system concerns, are likely to be more critical concerns than the given chip architecture.
I wanted to stipulate the importance of this second bullet before I begin my next topic because the same kind of concerns will apply to the functional programming paradigm discussion. Obviously, one shouldn’t accept theoretical limits/characteristics of a chip architecture as the sole decision point in choosing a chip architecture. However, I believe that core design decisions are hard to change down the road and so understanding BOTH short term AND long term, practical AND theoretical, trade-offs is the best course of action.
So the same goes for choosing a development language. I acknowledge up front that when it comes to developing secure software, having programmers with a strong understanding of secure programming is far more important than programming language choice. That being said, from a reliability, safety and security point of view, there are reasons for control system designers to consider employing the ‘new’ functional programming paradigm in their blue water systems.
So what is this ‘new’ ‘functional’ programming paradigm and what value does it bring to the control system world. The hard-core object orientation types will tell you that ‘functional’ programming is a step backwards to structured programming. I acknowledge that this might be in some sense true in the enterprise software domain where most hard-core object orientation types dwell. But, technically speaking, functional programming is different from structured programming in a couple of key ways which impact concurrent systems and reliability, safety & security critical control systems. A good definition of functional programming, also quoted on the Functional Programming wikipedia page, comes from Hudak who states:
In computer science, functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids state and mutable data. It emphasizes the application of functions, in contrast to the imperative programming style, which emphasizes changes in state.[2]
I see two key benefits to this paradigm from the reliability and security point of view. The first is a very general point that I will just state in passing, that is that the functional paradigm tends to discourage excessive maintenance of state which may lead to fewer side effects (this might be the driver for Ericsson’s Erlang functional language, because the telecom engineers are dealing with highly concurrent systems and the first rule of concurrent systems is that ‘state is hell’).
But the more critical point from a control systems reliablity, safety & security point of view is that functional programming is a paradigm that facilitates formal verification of systems. Despite decades of research, formal methods are still perceived to be excessively costly and cumbersome. With one notable exception, (use of ADA in the avionics system of the new Boeing 787 Dreamliner) very little has been published lately on the application of formal methods to industrial manufacturing & process systems. I suggest that the emergence of modern functional programming languages may reduce the cost of formal methods in industrial control technologies making formal methods for industrial control technologies cost effective.
Interestingly, one of the most notable adopters of functional programming languages to facilitate formal verification is Microsoft, which has created a modified version of the OCAML programming language they call F#.
For traditional places to learn more about functional programming in general you might want to check out OCAML, Haskell or the Symposium on Trends in Functional Programming.
To learn more about leveraging the functional programming paradigm to facilitate formal verification check out the ‘clean‘ programming language and specifically the ‘sparkle‘ tool.
And for a really cool project that specifically targets the application of functional programming to embedded systems check out the Hume project and one of it’s key progeny, the EmBounded project.