[langsec-discuss] langsec-discuss Digest, Vol 2, Issue 1
greyhatlisphacker at gmail.com
Sun Jun 3 18:23:27 UTC 2012
I Just thought I'd comment on the following as I've grown to
appreciate Ada and its features after learning about the security
problems that continue to infect the technical and computing
>It is worth mentioning that Ada is not particularly functional, as
>languages go. It's at its core a structured programming language, with
>object-oriented bits tacked on. Unlike C++, which has a very similar
>description, Ada also has a very strict yet expressive type system.
>All in all, it's a neat language, but not one that's particularly
>suited to langsec work
Language Theoretic Security, if I'm not mistaken, is simply
understanding that there are constraints that computational theory
places upon us as we write software. To be security conscious means
that we must be strict and explicit in what computations we want done,
and which computations we do not. To be strict means we can *prove*
our programs are correct -- ie. meet specification that determines
permissible computations to be done.
Ada is not popular among "hackers." It was not meant to be. It is
designed to make software reliable and easy to maintain. It is used
in areas where failure is *not* an option -- medical devices,
aviation, transportation, nuclear, and in military weapons systems.
These areas are know as having "high assurance" requirements, where
certain portions of the system, if not the entire project, are
mathematically proved as having particular security and reliability
properties. Ada supports this quite well, with a variety of tools
I'll describe in a bit.
If you are familiar with the Common Criteria, the types of projects
where Ada would be used have an Evaluation and Assurance Level of 5, 6
or 7. The vast majority of software is rather low on this scale -- 3
or 4 at the most.
Ada was designed for writing operating systems, embedded systems, low
level, bit twiddling software that requires an imperative approach for
managing the hardware most efficiently. It has supported concurrent
programming since '83, and OOP was added in 1995. More revisions
(minor ones) occurred in 2005 and are going on in 2012.
Ada has strong typing, as you mentioned. It supports formal
verification of the program. There is a rigorous subset of Ada known
as SPARK, which allows static analysis techniques to be applied to Ada
programs to pick up even more errors that could undermine program
reliaiblity at runtime.
An example where SPARK was used effectively:
Ada-derived Skein crypto shows SPARK
All of these great Ada tools are open source under the GPL. There is
nothing wrong with the language. The problem is that all computer
languages are part technology, and part religion.
More information about the langsec-discuss