seL4 as base of an AdaOS with some Spark proofing?

seL4 as base of an AdaOS with some Spark proofing?

[kug1977]

Hi, 

NICTA and General Dynamics C4 Systems have made seL4 Open Source (GPLv2/ BSD). seL4 is the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement and claims to be the world's most highly-assured OS.

As seL4 is written in C and some ASM and the proofing was done with Haskell, I asked myself: Can we use this kernel as a base to develop a real AdaOS with Spark to proof it's correctness? seL4 is a real microkernel, so it's not like porting Linux or Mach to Ada. 

L4 has Real-Time capabilities, a capability based security system, Task and Threads, high speed IPC, so it might fit everything from embedded to server. With Genode (http://genode.org/) there's a test environment with different kernels (incl. L4) and a tool chain, so we must not start from scratch. 

Doing an OS in Ada / Spark, might attract some people to use Ada instead of C. And having an OS written in Ada, seems not only my dream. :-)

-kug1977

Re: seL4 as base of an AdaOS with some Spark proofing?

[Georg Bauhaus]

On 30/07/14 10:22, kug1977@web.de wrote:
> Doing an OS in Ada / Spark, might attract some people to use Ada instead of C.

Having an OS in Ada / GNATSpark available online might attract
some people to use Ada / GNATSpark instead of C.

Having an OS written in C that is proven correct and available
online shows that Ada / GNATSpark is not needed any more.

That's the impression, on first sight, that would need to be overcome IMHO.
You'd need three universities to switch proof setups, including languages,
for no apparent reason.

Re: seL4 as base of an AdaOS with some Spark proofing?

[Peter Chapin]

On 2014-07-30 05:06, Georg Bauhaus wrote:

> Having an OS written in C that is proven correct and available
> online shows that Ada / GNATSpark is not needed any more.

It is not news that it is possible to prove certain C programs correct.
I refer you to the Frama-C project and it's deductive verification
plugins as one example.

The question one must ask is: how difficult is it to do and how much
"normal" code can you effectively prove?

Peter

Re: seL4 as base of an AdaOS with some Spark proofing?

[G.B.]

On 30.07.14 12:41, Peter Chapin wrote:

> The question one must ask is: how difficult is it to do and how much
> "normal" code can you effectively prove?

Questions about the efficiency of coding/reasoning could well
be made economically interesting, I think. In this seL4
scenario, one is proving formal source text, and measuring
this effort could be done by using wall clock time (as usual),
that is: person hours, and processor time.

Looking at what they show, e.g., no buffer overflows, no
problems with arithmetic, avoiding certain pointer issues,
one could compare the difficulties of preventing these mostly
by construction, i.e., scalar types of Ada + GNATSpark, and
not by proving things after the fact.

Re: seL4 as base of an AdaOS with some Spark proofing?

[Shark8]

On 30-Jul-14 02:22, kug1977@web.de wrote:
> NICTA and General Dynamics C4 Systems have made seL4 Open Source (GPLv2/ BSD).
> seL4 is the world's first operating-system kernel with an end-to-end proof of
> implementation correctness and security enforcement and claims to be the
> world's most highly-assured OS.

 From their FAQ:
> *What are the proof assumptions?*
>
> The brief version is: we assume that in-kernel assembly code is correct,
> hardware behaves correctly, in-kernel hardware management (TLB and caches) is
> correct, and boot code is correct. The hardware model assumes DMA to be off
> or to be trusted. The security proofs additionally give a list of conditions
> how the system is configured.

Note what they're assuming are correct:
(1) In-Kernel HW resource management,
(2) In-kernel ASM functions,
(3) Boot[-loader?] is correct.

That's not very reasonably an end-to-end proof; though #3 is arguable, 
I'll grant the DMA assumption is. -- With Ada/Spark we *can* do better.

Moreover, given Ada's (a) natural spec/body divide, (b) better 
numeric/enumeration model, and (c) generic facilities we can write it in 
a more portable manner than is possible w/ C.

Re: seL4 as base of an AdaOS with some Spark proofing?

[anon]

seL4 is just another  subset of the L4 project, which has nothing to 
do with Ada or an AdaOS.  Now, there are a number of Ada OS projects
which core code are based on the L4 project, like MaRTE (last update 
uses GNAT 2009), RTERMS (2008), and OpenRavencar (based on GNAT 3.13).

For Ada purest, to do a AdaOS, like the one I an working on, the entire 
code must be written in Ada with exceptions for macros for assembly code 
(using the Ada Machine_Code package) that extents Ada API to allow 
hardware instructions, such as the CPU's I/O instructions. And some of 
these macros instructions include code used to switch the processor from 
initial 8/16 bit 8086 state (power up/reset) to a 32-bit protected mode 
and then detects and if possible switch to 64-bit mode during the boot 
phase.

The AdaOS should be able to handle both 32-bit/64-bit code and maybe a 
some trusted special case protected VM code. As for languages, the 
OS should have Ada as the primary languages. If a secondary language is 
desired then it's compiler must be written in Ada. This means that 
others projects like openGL should be written in Ada instead of just 
porting the project code to the new AdaOS after a C compiler is 
written in Ada and then binding the code to the AdaOS.

The AdaOS, also should be a stand alone system that can work 
within a virtualization environments with some small limitations 
caused by the VM engine unless the VM is also, written in Ada and 
the AdaOS is the host OS.

Then there's the compiler while GNAT is an OK compiler it will not 
work for the new OS, we need a compiler from the ground up written in 
Ada that can produce code for a number of OS including an AdaOS that 
does not depends on any host OS or a design implementation like GNU 
which is based on C/C++. That way the new Ada compiler could be 
easily ported to the new OS without any other language or groups 
involvement.

But just having an AdaOS will not increase the usage of Ada. This 
might change if and only if the AdaOS was a complete and robust OS 
that could go against Microsoft Windows and Apple's OS X. But 
most people writing an AdaOS normally stop after they finish the 
initial kernel. Which mean an AdaOS will never become robust enough 
to even equal any OS used today. much less compete with those 
OS. 



In <791c07d0-575d-42be-ad5c-219aa3cf7734@googlegroups.com>, kug1977@web.de writes:
>Hi,=20
>
>NICTA and General Dynamics C4 Systems have made seL4 Open Source (GPLv2/ BS=
>D). seL4 is the world's first operating-system kernel with an end-to-end pr=
>oof of implementation correctness and security enforcement and claims to be=
> the world's most highly-assured OS.
>
>As seL4 is written in C and some ASM and the proofing was done with Haskell=
>, I asked myself: Can we use this kernel as a base to develop a real AdaOS =
>with Spark to proof it's correctness? seL4 is a real microkernel, so it's n=
>ot like porting Linux or Mach to Ada.=20
>
>L4 has Real-Time capabilities, a capability based security system, Task and=
> Threads, high speed IPC, so it might fit everything from embedded to serve=
>r. With Genode (http://genode.org/) there's a test environment with differe=
>nt kernels (incl. L4) and a tool chain, so we must not start from scratch.=
>=20
>
>Doing an OS in Ada / Spark, might attract some people to use Ada instead of=
> C. And having an OS written in Ada, seems not only my dream. :-)
>
>-kug1977

Re: seL4 as base of an AdaOS with some Spark proofing?

[Peter Chapin]

On 2014-07-30 13:47, Shark8 wrote:

> From their FAQ:
>> *What are the proof assumptions?*
>>
>> The brief version is: we assume that in-kernel assembly code is correct,
>> hardware behaves correctly, in-kernel hardware management (TLB and
>> caches) is
>> correct, and boot code is correct. The hardware model assumes DMA to
>> be off
>> or to be trusted. The security proofs additionally give a list of
>> conditions
>> how the system is configured.
> 
> Note what they're assuming are correct:
> (1) In-Kernel HW resource management,
> (2) In-kernel ASM functions,
> (3) Boot[-loader?] is correct.
> 
> That's not very reasonably an end-to-end proof; though #3 is arguable,
> I'll grant the DMA assumption is. -- With Ada/Spark we *can* do better.

I'm not clear what they mean by "in-kernel hardware management" here.
Are they talking about the hardware itself? If so, then SPARK would have
to make that assumption as well. Similarly SPARK would have to assume
any assembly language components are correct since they can't be
analyzed. Of course one hopes the size of such components is minimal.

I'm going to guess the seL4 people regarded the boot loader as outside
the scope of their project just as they might regard applications as
outside their scope. Of course a verified boot loader would be great...
but then so would be verified applications.

So it seems to me that any SPARK version of a verified OS would have to
make the same sort of high level assumptions, depending on what (1)
means, exactly.

Peter

Re: seL4 as base of an AdaOS with some Spark proofing?

[Shark8]

On 30-Jul-14 16:40, Peter Chapin wrote:
> I'm not clear what they mean by "in-kernel hardware management" here.
> Are they talking about the hardware itself? If so, then SPARK would have
> to make that assumption as well. Similarly SPARK would have to assume
> any assembly language components are correct since they can't be
> analyzed. Of course one hopes the size of such components is minimal.

If it was the HW itself I wouldn't have thought they would add 
'management' -- therefore I think it must be concluded they are talking 
about things like properly using the cache or hw-paging.

> I'm going to guess the seL4 people regarded the boot loader as outside
> the scope of their project just as they might regard applications as
> outside their scope. Of course a verified boot loader would be great...
> but then so would be verified applications.

I'm the one who added 'loader' as the original text was "boot code is 
correct" -- I assume it means the loader and I could grant that should 
be out of the scope of an OS; /HOWEVER/, it could also be the code which 
starts/initializes the OS, in which case I would have to say it 
certainly falls into the the scope of verifying the OS "end-to-end".

Re: seL4 as base of an AdaOS with some Spark proofing?

[Simon Clubley]

On 2014-07-30, Shark8 <OneWingedShark@gmail.com> wrote:
> On 30-Jul-14 02:22, kug1977@web.de wrote:
>> NICTA and General Dynamics C4 Systems have made seL4 Open Source (GPLv2/ BSD).
>> seL4 is the world's first operating-system kernel with an end-to-end proof of
>> implementation correctness and security enforcement and claims to be the
>> world's most highly-assured OS.
>
>  From their FAQ:
>> *What are the proof assumptions?*
>>
>> The brief version is: we assume that in-kernel assembly code is correct,
>> hardware behaves correctly, in-kernel hardware management (TLB and caches) is
>> correct, and boot code is correct. The hardware model assumes DMA to be off
>> or to be trusted. The security proofs additionally give a list of conditions
>> how the system is configured.
>
> Note what they're assuming are correct:
> (1) In-Kernel HW resource management,

TLB and cache management can be a _real_ pain on current processors.
I don't know how much you know about this, but a good example to examine
is the Cortex-A8 series. A specific example is the AM3359 MCU used in
the Beaglebone Black.

> (2) In-kernel ASM functions,

It's not clear if they mean some assembly language kernel functions or
if they are talking about the generated code from the compiler.

> (3) Boot[-loader?] is correct.
>

You forgot:

(4) "hardware behaves correctly" - IOW there's no nasty surprises waiting
for you in the MCU specific errata list.

> That's not very reasonably an end-to-end proof; though #3 is arguable, 
> I'll grant the DMA assumption is. -- With Ada/Spark we *can* do better.
>
> Moreover, given Ada's (a) natural spec/body divide, (b) better 
> numeric/enumeration model, and (c) generic facilities we can write it in 
> a more portable manner than is possible w/ C.

It's true that Ada gives you more tools than C does here, but none of
that helps you get the TLB and cache management correct. :-)

It also doesn't help you with any security issues within the hardware
itself. For example, do you trust any hardware specific RNGs ?
Are there any hardware specific security issues such as the SMM on x86
processors ?

Simon.

-- 
Simon Clubley, clubley@remove_me.eisner.decus.org-Earth.UFP
Microsoft: Bringing you 1980s technology to a 21st century world

Re: seL4 as base of an AdaOS with some Spark proofing?

[Georg Bauhaus]

On 31/07/14 02:31, Simon Clubley wrote:
>> >(2) In-kernel ASM functions,
> It's not clear if they mean some assembly language kernel functions or
> if they are talking about the generated code from the compiler.
>

They explain that every kernel must have some assembly
language in it, and that theirs has some 300 lines of assembly.

Sounds like one can prove this amount of assembly code correct?

Re: seL4 as base of an AdaOS with some Spark proofing?

[gvdschoot]

On Wednesday, July 30, 2014 7:58:33 PM UTC+2, an...@att.net wrote:
> seL4 is just another  subset of the L4 project, which has nothing to 
> 
> do with Ada or an AdaOS.  Now, there are a number of Ada OS projects
> 
> which core code are based on the L4 project, like MaRTE (last update 
> 
> uses GNAT 2009), RTERMS (2008), and OpenRavencar (based on GNAT 3.13).
> 
> 
> 
> For Ada purest, to do a AdaOS, like the one I an working on, the entire 
> 
> code must be written in Ada with exceptions for macros for assembly code 
> 
> (using the Ada Machine_Code package) that extents Ada API to allow 
> 
> hardware instructions, such as the CPU's I/O instructions. And some of 
> 
> these macros instructions include code used to switch the processor from 
> 
> initial 8/16 bit 8086 state (power up/reset) to a 32-bit protected mode 
> 
> and then detects and if possible switch to 64-bit mode during the boot 
> 
> phase.
> 
> 
> 
> The AdaOS should be able to handle both 32-bit/64-bit code and maybe a 
> 
> some trusted special case protected VM code. As for languages, the 
> 
> OS should have Ada as the primary languages. If a secondary language is 
> 
> desired then it's compiler must be written in Ada. This means that 
> 
> others projects like openGL should be written in Ada instead of just 
> 
> porting the project code to the new AdaOS after a C compiler is 
> 
> written in Ada and then binding the code to the AdaOS.
> 
> 
> 
> The AdaOS, also should be a stand alone system that can work 
> 
> within a virtualization environments with some small limitations 
> 
> caused by the VM engine unless the VM is also, written in Ada and 
> 
> the AdaOS is the host OS.
> 
> 
> 
> Then there's the compiler while GNAT is an OK compiler it will not 
> 
> work for the new OS, we need a compiler from the ground up written in 
> 
> Ada that can produce code for a number of OS including an AdaOS that 
> 
> does not depends on any host OS or a design implementation like GNU 
> 
> which is based on C/C++. That way the new Ada compiler could be 
> 
> easily ported to the new OS without any other language or groups 
> 
> involvement.
> 
> 
> 
> But just having an AdaOS will not increase the usage of Ada. This 
> 
> might change if and only if the AdaOS was a complete and robust OS 
> 
> that could go against Microsoft Windows and Apple's OS X. But 
> 
> most people writing an AdaOS normally stop after they finish the 
> 
> initial kernel. Which mean an AdaOS will never become robust enough 
> 
> to even equal any OS used today. much less compete with those 
> 
> OS. 
> 

So you want to compete with the big guys? You want to compete with the multi billion dollar companies? With what? Ideas? Do you know how many man years it takes? Let's just forget the desktop or tablet. These areas are untouchable unless you are very lucky.

Here is another idea. Let's for instance instead focus on tools that can automatically translate C source code to Ada.

Re: seL4 as base of an AdaOS with some Spark proofing?

[kug1977]

> So you want to compete with the big guys? You want to compete with the multi billion dollar companies? With what? Ideas? Do you know how many man years it takes? 

Well, I remember a time an unknown student posted something about a unix kernel and a big fellow in theoretical OS design called the idea stupid. Today it's the most used OS in Servers and embedded products. And it's not an microkernel, so more code then L4. 

The idea was, that if we show, that you can do a whole microkernel in Ada (and some part on top of it are written in Ada/ Spark, i.e. ironsides (DNS), AWS (WebServer), we can show, how to make a secure OS everybody is talking about, but nobody can deliver at the moment.

And having L4 microkernel make the source code smaller. At the beginning we have to use parts of other OSes, we have to integrate C code  and critical part should moved over to Ada sooner than later, but it's a better situation than Linux and BSD were in in the 1990er.

I know, that a lot of work has to be done. But L4 is a proven design. A lot of design decision are done and we can learn from the mistakes they've done. Nobody has to start from "primordial soup" of OS design, it more a change of the implementation language.

> Here is another idea. Let's for instance instead focus on tools that can automatically translate C source code to Ada.

What I know about C, you won't and I'm very sure you can't translate it to Ada in an automatic way. But you can use the seL4 code base and migrate it to Ada and use the Haskell Code to see, where the "big money" put the effort in to check correctness. And as written before, a lot of checks we can forgett, because they are part of Ada already. So the code base should shrink. 

-kug1977

Re: seL4 as base of an AdaOS with some Spark proofing?

[gvdschoot]

On Friday, August 1, 2014 9:42:03 AM UTC+2, kug...@web.de wrote:
> > So you want to compete with the big guys? You want to compete with the multi billion dollar companies? With what? Ideas? Do you know how many man years it takes? 
> 
> Well, I remember a time an unknown student posted something about a unix kernel and a big fellow in theoretical OS design called the idea stupid. Today it's the most used OS in Servers and embedded products. And it's not an microkernel, so more code then L4. 
> 

I also said: "These areas are untouchable unless you are very lucky."
The problem with Linus Torvalds is that he doesn't scale very well. The same with RMS.

> The idea was, that if we show, that you can do a whole microkernel in Ada (and some part on top of it are written in Ada/ Spark, i.e. ironsides (DNS), AWS (WebServer), we can show, how to make a secure OS everybody is talking about, but nobody can deliver at the moment.

I like that idea.

> And having L4 microkernel make the source code smaller. At the beginning we have to use parts of other OSes, we have to integrate C code  and critical part should moved over to Ada sooner than later, but it's a better situation than Linux and BSD were in in the 1990er.

I am not sure having a microkernel makes the overall code size smaller. You still need drivers, filesystems etc.. They only don't run in the critical path.

Another benefit of microkernels is that it doesn't matter in what language a server is written in. A mixed C / Ada / lang-x is perfectly fine.

What I would like to say is that having a running system is very important. From there on things can gradually improve.

> I know, that a lot of work has to be done. But L4 is a proven design. A lot of design decision are done and we can learn from the mistakes they've done. Nobody has to start from "primordial soup" of OS design, it more a change of the implementation language.

For the kernel yes. But if you want a complete OS, there are a lot of things more. GUI for instance is a can of worms. To POSIX or not to POSIX? Alienate because of security or accept a wide range of attack surfaces?

> > Here is another idea. Let's for instance instead focus on tools that can automatically translate C source code to Ada.
> 
> What I know about C, you won't and I'm very sure you can't translate it to Ada in an automatic way. But you can use the seL4 code base and migrate it to Ada and use the Haskell Code to see, where the "big money" put the effort in to check correctness. And as written before, a lot of checks we can forgett, because they are part of Ada already. So the code base should shrink. 

Just because it hasn't been done before doesn't mean it is impossible. For instance the Go (golang) team in the person of Russ Cox is working on c2go and the approach he takes is unconventional. There is presentation about this on youtube.

However if C and Ada can coexist there is no need for it to get a system up and running.

The major problem that I see is the organization. The only thing we are doing right now is talking.

Re: seL4 as base of an AdaOS with some Spark proofing?

[gvdschoot]

Talking about a running system. Minix3 is just that.

Re: seL4 as base of an AdaOS with some Spark proofing?

[anon]

Yes, an AdaOS should be written and complete with the big OS(s). 

The problem is the older OS are using old outdate techniques and 
technology. Micosoft Windows is a blending of Win 95/98 
(aka Micosoft[DOS]/IBM(Windows), 1980(s)) and NT (aka DEC VAX, 1980) 
software. Then you have AT&T old OS (1969) children. which includes 
the licensed Sun Solaris OS or IBM AIX, and then BSD groups like 
Apple's OS X, and Darwin ( open source ) or the open source BSD(s) 
FreeBSD, OpenBSD, NetBSD. All which use software technique from 1960(s) .. 
1970(s).  Then you have Linux written using techniques and technology
from the 1990(s). And you can include IBM Z/OS which is basically 
just a 64-bit port of MVS and still has it core from from the 1960s.

So, there is no OS for the 22nd century. And all of these older OS 
have problem which hackers can use to harm the system or steal data. 
We need a OS that can handle the current hardware and system designs 
and be modular enough to allow complete change for the future. But 
be strong enough to allow the design and implement a security 
system that can handle current attack as well as being modular to 
update itself (using AI and other tools) for the hackers of the 
future.

So why not use (non-oops) Ada to write this new operating system? 
One could allow the special constructs in Ada to bind the OS to like 
tasking, interrupts to the hardware while allowing the software 
to protect the system and data.  And Dewar once stated, if you can 
write the code in C then you can write the code in Ada. And if you 
limit the assembly code to special hardware packages such as boot 
up routine and use Ada Machine_Code, one could only have to re-write 
these special packages to port the OS to another processor.


Note: Hacker could be software or human trying to gain access or 
destroy the system.

Note: Why non-oops Ada. Most OS writers understand that using oops 
decrease the level of security to around 10 .. 20%.  It's one reason 
why even Microsoft will not allow oops in its kernel. And every time 
they use oops in IE, it contains a number of security holes.

And translating C to Ada. People will just say stay with the first language!

In <9509bda5-4429-4e2c-ac97-bc7959257006@googlegroups.com>, gvdschoot@gmail.com writes:
>On Wednesday, July 30, 2014 7:58:33 PM UTC+2, an...@att.net wrote:
>> seL4 is just another  subset of the L4 project, which has nothing to=20
>>=20
>> do with Ada or an AdaOS.  Now, there are a number of Ada OS projects
>>=20
>> which core code are based on the L4 project, like MaRTE (last update=20
>>=20
>> uses GNAT 2009), RTERMS (2008), and OpenRavencar (based on GNAT 3.13).
>>=20
>>=20
>>=20
>> For Ada purest, to do a AdaOS, like the one I an working on, the entire=
>=20
>>=20
>> code must be written in Ada with exceptions for macros for assembly code=
>=20
>>=20
>> (using the Ada Machine_Code package) that extents Ada API to allow=20
>>=20
>> hardware instructions, such as the CPU's I/O instructions. And some of=20
>>=20
>> these macros instructions include code used to switch the processor from=
>=20
>>=20
>> initial 8/16 bit 8086 state (power up/reset) to a 32-bit protected mode=
>=20
>>=20
>> and then detects and if possible switch to 64-bit mode during the boot=20
>>=20
>> phase.
>>=20
>>=20
>>=20
>> The AdaOS should be able to handle both 32-bit/64-bit code and maybe a=20
>>=20
>> some trusted special case protected VM code. As for languages, the=20
>>=20
>> OS should have Ada as the primary languages. If a secondary language is=
>=20
>>=20
>> desired then it's compiler must be written in Ada. This means that=20
>>=20
>> others projects like openGL should be written in Ada instead of just=20
>>=20
>> porting the project code to the new AdaOS after a C compiler is=20
>>=20
>> written in Ada and then binding the code to the AdaOS.
>>=20
>>=20
>>=20
>> The AdaOS, also should be a stand alone system that can work=20
>>=20
>> within a virtualization environments with some small limitations=20
>>=20
>> caused by the VM engine unless the VM is also, written in Ada and=20
>>=20
>> the AdaOS is the host OS.
>>=20
>>=20
>>=20
>> Then there's the compiler while GNAT is an OK compiler it will not=20
>>=20
>> work for the new OS, we need a compiler from the ground up written in=20
>>=20
>> Ada that can produce code for a number of OS including an AdaOS that=20
>>=20
>> does not depends on any host OS or a design implementation like GNU=20
>>=20
>> which is based on C/C++. That way the new Ada compiler could be=20
>>=20
>> easily ported to the new OS without any other language or groups=20
>>=20
>> involvement.
>>=20
>>=20
>>=20
>> But just having an AdaOS will not increase the usage of Ada. This=20
>>=20
>> might change if and only if the AdaOS was a complete and robust OS=20
>>=20
>> that could go against Microsoft Windows and Apple's OS X. But=20
>>=20
>> most people writing an AdaOS normally stop after they finish the=20
>>=20
>> initial kernel. Which mean an AdaOS will never become robust enough=20
>>=20
>> to even equal any OS used today. much less compete with those=20
>>=20
>> OS.=20
>>=20
>
>So you want to compete with the big guys? You want to compete with the mult=
>i billion dollar companies? With what? Ideas? Do you know how many man year=
>s it takes? Let's just forget the desktop or tablet. These areas are untouc=
>hable unless you are very lucky.
>
>Here is another idea. Let's for instance instead focus on tools that can au=
>tomatically translate C source code to Ada.

Re: seL4 as base of an AdaOS with some Spark proofing?

[Randy Brukardt]

<gvdschoot@gmail.com> wrote in message 
news:485a93a1-8920-4139-8563-591dba79d68d@googlegroups.com...
On Friday, August 1, 2014 9:42:03 AM UTC+2, kug...@web.de wrote:
...
>> > Here is another idea. Let's for instance instead focus on tools that 
>> > can automatically translate C source code to Ada.
>>
>> What I know about C, you won't and I'm very sure you can't translate it 
>> to Ada in an automatic way.

Of course you can translate C to Ada. There were various tools to do that 
back in the 1980s. The problem is that the Ada you get is terrible Ada (the 
one I saw was full of address manipulations). (That's true of any automatic 
language translator, BTW.)

>Just because it hasn't been done before doesn't mean it is impossible. For 
>instance the
> Go (golang) team in the person of Russ Cox is working on c2go and the 
> approach he
> takes is unconventional. There is presentation about this on youtube.

There's no problem doing such a translator (it's relatively easy to do). The 
problem is that the result is terrible Ada (little typing, lots of address 
math, etc.). In order to make *good* Ada, you need a redesign. That's also 
the case if you want to use SPARK or even the Ada 2012 contracts -- a 
translator can't create intentions that aren't in the source code. There's a 
reason such translators today stop at thin bindings -- that's because there 
is no point in going further without a redesign (and thin bindings ought to 
always be wrapped in a thick binding for Ada use).

                                  Randy.