* seL4 as base of an AdaOS with some Spark proofing? @ 2014-07-30 8:22 kug1977 2014-07-30 9:06 ` Georg Bauhaus ` (2 more replies) 0 siblings, 3 replies; 16+ messages in thread From: kug1977 @ 2014-07-30 8:22 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-07-30 8:22 seL4 as base of an AdaOS with some Spark proofing? kug1977 @ 2014-07-30 9:06 ` Georg Bauhaus 2014-07-30 10:41 ` Peter Chapin 2014-07-30 17:47 ` Shark8 2014-07-30 17:58 ` anon 2 siblings, 1 reply; 16+ messages in thread From: Georg Bauhaus @ 2014-07-30 9:06 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-07-30 9:06 ` Georg Bauhaus @ 2014-07-30 10:41 ` Peter Chapin 2014-07-30 11:55 ` G.B. 0 siblings, 1 reply; 16+ messages in thread From: Peter Chapin @ 2014-07-30 10:41 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-07-30 10:41 ` Peter Chapin @ 2014-07-30 11:55 ` G.B. 0 siblings, 0 replies; 16+ messages in thread From: G.B. @ 2014-07-30 11:55 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-07-30 8:22 seL4 as base of an AdaOS with some Spark proofing? kug1977 2014-07-30 9:06 ` Georg Bauhaus @ 2014-07-30 17:47 ` Shark8 2014-07-30 22:40 ` Peter Chapin 2014-07-31 0:31 ` Simon Clubley 2014-07-30 17:58 ` anon 2 siblings, 2 replies; 16+ messages in thread From: Shark8 @ 2014-07-30 17:47 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-07-30 17:47 ` Shark8 @ 2014-07-30 22:40 ` Peter Chapin 2014-07-30 22:53 ` Shark8 2014-07-31 0:31 ` Simon Clubley 1 sibling, 1 reply; 16+ messages in thread From: Peter Chapin @ 2014-07-30 22:40 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-07-30 22:40 ` Peter Chapin @ 2014-07-30 22:53 ` Shark8 0 siblings, 0 replies; 16+ messages in thread From: Shark8 @ 2014-07-30 22:53 UTC (permalink / raw) 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". ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-07-30 17:47 ` Shark8 2014-07-30 22:40 ` Peter Chapin @ 2014-07-31 0:31 ` Simon Clubley 2014-07-31 6:23 ` Georg Bauhaus 1 sibling, 1 reply; 16+ messages in thread From: Simon Clubley @ 2014-07-31 0:31 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-07-31 0:31 ` Simon Clubley @ 2014-07-31 6:23 ` Georg Bauhaus 0 siblings, 0 replies; 16+ messages in thread From: Georg Bauhaus @ 2014-07-31 6:23 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-07-30 8:22 seL4 as base of an AdaOS with some Spark proofing? kug1977 2014-07-30 9:06 ` Georg Bauhaus 2014-07-30 17:47 ` Shark8 @ 2014-07-30 17:58 ` anon 2014-07-31 22:03 ` gvdschoot 2 siblings, 1 reply; 16+ messages in thread From: anon @ 2014-07-30 17:58 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-07-30 17:58 ` anon @ 2014-07-31 22:03 ` gvdschoot 2014-08-01 7:42 ` kug1977 2014-08-01 19:17 ` anon 0 siblings, 2 replies; 16+ messages in thread From: gvdschoot @ 2014-07-31 22:03 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-07-31 22:03 ` gvdschoot @ 2014-08-01 7:42 ` kug1977 2014-08-01 8:27 ` gvdschoot 2014-08-01 19:17 ` anon 1 sibling, 1 reply; 16+ messages in thread From: kug1977 @ 2014-08-01 7:42 UTC (permalink / raw) > 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-08-01 7:42 ` kug1977 @ 2014-08-01 8:27 ` gvdschoot 2014-08-01 9:04 ` gvdschoot 2014-08-01 19:32 ` Randy Brukardt 0 siblings, 2 replies; 16+ messages in thread From: gvdschoot @ 2014-08-01 8:27 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-08-01 8:27 ` gvdschoot @ 2014-08-01 9:04 ` gvdschoot 2014-08-01 19:32 ` Randy Brukardt 1 sibling, 0 replies; 16+ messages in thread From: gvdschoot @ 2014-08-01 9:04 UTC (permalink / raw) Talking about a running system. Minix3 is just that. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-08-01 8:27 ` gvdschoot 2014-08-01 9:04 ` gvdschoot @ 2014-08-01 19:32 ` Randy Brukardt 1 sibling, 0 replies; 16+ messages in thread From: Randy Brukardt @ 2014-08-01 19:32 UTC (permalink / raw) <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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: seL4 as base of an AdaOS with some Spark proofing? 2014-07-31 22:03 ` gvdschoot 2014-08-01 7:42 ` kug1977 @ 2014-08-01 19:17 ` anon 1 sibling, 0 replies; 16+ messages in thread From: anon @ 2014-08-01 19:17 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
end of thread, other threads:[~2014-08-01 19:32 UTC | newest] Thread overview: 16+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2014-07-30 8:22 seL4 as base of an AdaOS with some Spark proofing? kug1977 2014-07-30 9:06 ` Georg Bauhaus 2014-07-30 10:41 ` Peter Chapin 2014-07-30 11:55 ` G.B. 2014-07-30 17:47 ` Shark8 2014-07-30 22:40 ` Peter Chapin 2014-07-30 22:53 ` Shark8 2014-07-31 0:31 ` Simon Clubley 2014-07-31 6:23 ` Georg Bauhaus 2014-07-30 17:58 ` anon 2014-07-31 22:03 ` gvdschoot 2014-08-01 7:42 ` kug1977 2014-08-01 8:27 ` gvdschoot 2014-08-01 9:04 ` gvdschoot 2014-08-01 19:32 ` Randy Brukardt 2014-08-01 19:17 ` anon
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox