<HTML><HEAD></HEAD>
<BODY dir=ltr bgColor=#ffffff>
<DIV dir=ltr>
<DIV style="FONT-SIZE: 12pt; FONT-FAMILY: 'Calibri'; COLOR: #000000">
<DIV>Hi Ken,</DIV>
<DIV> </DIV>
<DIV>Capability based HW ? Sounds interesting, any examples
? How does the HW handle stack corruption for calls , do you use
some register window scheme ? </DIV>
<DIV> </DIV>
<DIV>I may have it wrong but the idea of changing every procedure call into a
ipc call seems expensive to me and specialized HW has not done well over the
years. I have seen something similar attempted in some (poor) SOA
implementations where every class becomes a service and it tends to be a
disaster.. that said with multi cores , Async runtimes and fast IPC it
maybe possible.</DIV>
<DIV>I do believe the future is in breaking apps down into smaller
services that communicate asynchronously via IPC which a run time manages
, load balances , schedules etc These services would consist of several
methods . Classes with Heavy communication between them are normally in the same
service. This is already happening now witness browsers using multiple
processes for pages , and either banning ( IE10/Apple) or isolating add
ins. </DIV>
<DIV> </DIV>
<DIV>Also if we have a verified compiler ( a BIG if) then wouldn't a language
guarantee be enough ? Isnt this easier than new forms of HW ?</DIV>
<DIV> </DIV>
<DIV> </DIV>
<DIV>Ben</DIV>
<DIV
style="FONT-SIZE: small; TEXT-DECORATION: none; FONT-FAMILY: 'Calibri'; COLOR: #000000; FONT-WEIGHT: normal; FONT-STYLE: normal; DISPLAY: inline">
<DIV style="FONT: 10pt tahoma">
<DIV><FONT size=3 face=Calibri></FONT> </DIV>
<DIV style="BACKGROUND: #f5f5f5">
<DIV style="font-color: black"><B>From:</B> <A title=ken@sipantic.net
href="mailto:ken@sipantic.net">Ken</A> </DIV>
<DIV><B>Sent:</B> Friday, September 30, 2011 2:40 AM</DIV>
<DIV><B>To:</B> <A title=bklooste@gmail.com href="mailto:bklooste@gmail.com">Ben
Kloosterman</A> ; <A title=cap-talk@mail.eros-os.org
href="mailto:cap-talk@mail.eros-os.org">General discussions concerning
capability systems.</A> </DIV>
<DIV><B>Cc:</B> <A title=strohm@airmail.net
href="mailto:strohm@airmail.net">John R. Strohm</A> ; <A
title=cap-talk@mail.eros-os.org href="mailto:cap-talk@mail.eros-os.org">General
discussions concerning capability systems.</A> </DIV>
<DIV><B>Subject:</B> Re: [cap-talk] [friam] RE: Hoare's 1980 Turing Award
Lecture ...andprogram verification mea culpa</DIV></DIV></DIV>
<DIV> </DIV></DIV>
<DIV
style="FONT-SIZE: small; TEXT-DECORATION: none; FONT-FAMILY: 'Calibri'; COLOR: #000000; FONT-WEIGHT: normal; FONT-STYLE: normal; DISPLAY: inline">
<DIV>Ben et al</DIV>
<DIV>I agree with all the points you make. I would go a step further. The only
way to do what is actually needed, in a solid and consistent way, is to inherit
both verification and validation from capability based hardware. I know because
i have seen it work. </DIV>
<DIV>The alignment of goals can be reliably achieved when the hardware
guarantees subroutine level containment and detailed context sensitive
protection from the hard edge of cyberspace. Linear VM must be replaced as
part of this change. Cyberspace is atomic not linear. </DIV>
<DIV>Everything today is based on trust without any big stick to enforce best
practices and only super human special cases come close from time to time, in
point solutions that do not pass the test of time. </DIV>
<DIV>In a dynamically evolving world the specification of new requirements
arrive daily so V&V must come for free and be enforced by a common
denominator that cannot be bypassed this means hardware enforcement of
best practices. Programming must focus on new features. The platform must
guarantee cyber security for all to use and to misuse at the same time. </DIV>
<DIV>I see this only getting more critical as technology changes ever faster.
</DIV>
<DIV>The good solutions will rise to the top in the end. <BR>k<BR>Sent from my
iPhone</DIV>
<DIV><BR>On Sep 29, 2011, at 11:03 AM, "Ben Kloosterman" <<A
href="mailto:bklooste@gmail.com">bklooste@gmail.com</A>> wrote:<BR><BR></DIV>
<DIV></DIV>
<BLOCKQUOTE type="cite">
<DIV>
<DIV dir=ltr>
<DIV style="FONT-SIZE: 12pt; FONT-FAMILY: 'Calibri'; COLOR: #000000">
<DIV>Nothing casual about the financial markets where the wrong code can cost
millions but not being able to rapidly make changes can also cost big
time. And specs change quickly , even in the military the Ewacs failed
on day 1 of the gulf war and the specs were changed immediately. eg lives
depended on a new spec being written and implemented in hours .,. </DIV>
<DIV> </DIV>
<DIV>If your talking space how about Apollo 13 a modern version may
benefit from a new computer upload to re-manage power, compare
make a few changes run your unit tests and upload all with 12 hours..
This is difficult to do with verification and if you skipped the verification
you would be relying on no automated testing. </DIV>
<DIV> </DIV>
<DIV>Also many critical systems are very simple and often
implemented in HW circuits not code so verification is not an option .
</DIV>
<DIV> </DIV>
<DIV>What im really saying is it the arguments for verification are not that
simple</DIV>
<DIV>eg </DIV>
<UL>
<LI>for 100K of C + verification vs Java/C# and TDD , a
type safe and memory safe language will have far less issues
given equal resources.
<LI>Absolutely key conditions like you mention can be tested with TDD or
ensured with a few guards in the code.
<LI>Verification does not protect against compiler errors , TDD does
! So your 600 lines verified code has a 300K unverified dependency
<LI>Verification provides an expectation that it will work (TDD does
not) , which may lead to reduced testing and false confidence. There
can be errors in the compiler, specification , assumption's on 3rd party
systems or the verification .
<LI>Verification makes change very expensive , which means important things
don't get done. Look at Nuclear power plants , errors happened
in Japan and Russia which a more modern software system may have
prevented. eg the static nature cost lives.
<LI>TDD can evolve to handle the behaviour of other systems which may change
( and may not be verified)
<LI>Verification works on older languages/assembly which have more security
holes, eg don't even come close to ocap and the programs don't degrade
nicely..
<LI>Anyone written a verifier which supports multi threaded code ?
Having 2 cores and threads ( especially with a scheme like E) can
provide resiliency and cover HW failures without switching to a backup unit
yet ( which is always problematic) . Likewise simple stateless code and
simple clusters can provide excellent resilience., proving a load balancer
would be something nice that should be proven and verified . Than several
embedded machines would provide far greater work continuously </LI></UL>
<DIV> </DIV>
<DIV>OK i wouldn't do this for mission critical code because im not that brave
and few people have done it , but more should.</DIV>
<DIV> </DIV>
<DIV>Ben</DIV>
<DIV> </DIV>
<DIV
style="FONT-SIZE: small; TEXT-DECORATION: none; FONT-FAMILY: 'Calibri'; COLOR: #000000; FONT-WEIGHT: normal; FONT-STYLE: normal; DISPLAY: inline">
<DIV style="FONT: 10pt tahoma">
<DIV> </DIV>
<DIV style="BACKGROUND: #f5f5f5">
<DIV style="font-color: black"><B>From:</B> <A title=strohm@airmail.net
href="mailto:strohm@airmail.net">John R. Strohm</A> </DIV>
<DIV><B>Sent:</B> Thursday, September 29, 2011 9:06 PM</DIV>
<DIV><B>To:</B> <A title=bklooste@gmail.com
href="mailto:bklooste@gmail.com">Ben Kloosterman</A> ; <A
title=cap-talk@mail.eros-os.org
href="mailto:cap-talk@mail.eros-os.org">General discussions concerning
capability systems.</A> </DIV>
<DIV><B>Subject:</B> Re: [cap-talk] [friam] RE: Hoare's 1980 Turing Award
Lecture ...andprogram verification mea culpa</DIV></DIV></DIV>
<DIV> </DIV></DIV>
<DIV
style="FONT-SIZE: small; TEXT-DECORATION: none; FONT-FAMILY: 'Calibri'; COLOR: #000000; FONT-WEIGHT: normal; FONT-STYLE: normal; DISPLAY: inline">
<DIV dir=ltr>
<DIV style="FONT-SIZE: 12pt; FONT-FAMILY: 'Calibri'; COLOR: #000000">
<DIV>If your domain of discussion is CASUAL business programming, this may be
true.</DIV>
<DIV> </DIV>
<DIV>When your domain of discussion is safety-critical systems, with human
lives riding on them, those specs do not change anywhere near as
fluidly.</DIV>
<DIV> </DIV>
<DIV>The airplane must fly. It must operate in coordinated controlled
flight.</DIV>
<DIV> </DIV>
<DIV>The rocket motor must not be commanded to start unless BOTH keys have
been turned and BOTH launch switches depressed and the silo door is
OPEN. Observe that a system that never started the motor under any
circumstances would meet a casual interpretation of that specification.
This is almost exactly the system that NASA managed to build for one of the
Gemini launches. An unexpected failure left them with an interesting
piece of modern art and a major exercise in defeating their own safety
interlocks.</DIV>
<DIV> </DIV>
<DIV>The implanted pacemaker must pulse correctly, continuously.
Rebooting is not an option.</DIV>
<DIV
style="FONT-SIZE: small; TEXT-DECORATION: none; FONT-FAMILY: 'Calibri'; COLOR: #000000; FONT-WEIGHT: normal; FONT-STYLE: normal; DISPLAY: inline">
<DIV style="FONT: 10pt tahoma"><FONT size=3 face=Calibri></FONT></DIV>
<DIV
style="FONT-SIZE: small; TEXT-DECORATION: none; FONT-FAMILY: 'Calibri'; COLOR: #000000; FONT-WEIGHT: normal; FONT-STYLE: normal; DISPLAY: inline"> </DIV></DIV></DIV></DIV></DIV></DIV></DIV></DIV></BLOCKQUOTE>
<BLOCKQUOTE type="cite">
<DIV><SPAN>_______________________________________________</SPAN><BR><SPAN>cap-talk
mailing list</SPAN><BR><SPAN><A
href="mailto:cap-talk@mail.eros-os.org">cap-talk@mail.eros-os.org</A></SPAN><BR><SPAN><A
href="http://www.eros-os.org/mailman/listinfo/cap-talk">http://www.eros-os.org/mailman/listinfo/cap-talk</A></SPAN><BR></DIV></BLOCKQUOTE></DIV></DIV></DIV></BODY></HTML>