From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 2002:a24:47c7:: with SMTP id t190-v6mr6953063itb.35.1525110240703; Mon, 30 Apr 2018 10:44:00 -0700 (PDT) X-Received: by 2002:a9d:70d1:: with SMTP id w17-v6mr478945otj.5.1525110240452; Mon, 30 Apr 2018 10:44:00 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.uzoreto.com!weretis.net!feeder6.news.weretis.net!feeder.usenetexpress.com!feeder-in1.iad1.usenetexpress.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!f63-v6no2346739itc.0!news-out.google.com!15-v6ni3553itg.0!nntp.google.com!f63-v6no2346735itc.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Mon, 30 Apr 2018 10:44:00 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=47.185.233.194; posting-account=zwxLlwoAAAChLBU7oraRzNDnqQYkYbpo NNTP-Posting-Host: 47.185.233.194 References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com> <87k1su7nag.fsf@nightsong.com> <87po2la2qt.fsf@nightsong.com> <87in8buttb.fsf@jacob-sparre.dk> <3f7a7f76-c5eb-4cba-9051-6b5dfeeb906c@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: How to get Ada to ?cross the chasm?? From: "Dan'l Miller" Injection-Date: Mon, 30 Apr 2018 17:44:00 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Received-Bytes: 5583 X-Received-Body-CRC: 525867471 Xref: reader02.eternal-september.org comp.lang.ada:51849 Date: 2018-04-30T10:44:00-07:00 List-Id: On Monday, April 30, 2018 at 11:56:54 AM UTC-5, Jeffrey R. Carter wrote: > On 04/30/2018 03:06 PM, Simon Clubley wrote: > >=20 > > Software does become stale when it starts getting probed for security > > issues in new ways and you need to fix the security issue that laid > > unfixed or years or even decades and maybe do a redesign to fix any > > underlying problems. >=20 > S/W that is correct and reliable has no security issues, by definition. Software isn't written (yet) by definitions. Software is currently written= as a manual tradecraft by human beings who at best hold an axiom system in= their mind when crafting their design and their lines of code (and at wors= t hold vague rules of thumb as a perceived reference model of how the under= lying machine is thought to work; Nancy Leveson goes into the necessity of = this obfuscating-the-details mental model in her book _Safeware: System saf= ety and computers_). For example, if mandatory Harvard architectures* were the norm when the ope= rating system's source code was authored (e.g., ARM), then the operating sy= stem is ported to a von Neumann architecture** (e.g., Intel, AMD with ), th= en suddenly the operating system's underlying axiom system changed beneath = it at the hardware level. Suddenly, the operating system is oblivious to t= he need to inhibit data from being executable machine instructions. This i= s an example of Simon Clubley's =E2=80=9Cprobing for security issues in new= ways=E2=80=9D. An extant example of the reverse direction effectively occ= urred when Intel & AMD & ARM & POWER & Alpha & SPARC all added their variou= s-named analogues of NX bit to emulate Harvard architecture protections on = a von Neumann architecture. Then suddenly operating systems had the securi= ty axiom system shifted underneath them to properly securely enact a de fac= to Harvard architecture when they had insecurely assumed von Neumann up un= til that point. https://en.wikipedia.org/wiki/NX_bit https://en.wikipedia.org/wiki/Harvard_architecture https://en.wikipedia.org/wiki/Modified_Harvard_architecture https://en.wikipedia.org/wiki/Von_Neumann_architecture > > This is a CLI, not a library, but it demonstrates the point: > >=20 > > http://cve.mitre.org/cgi-bin/cvename.cgi?name=3DCVE-2017-17482 > >=20 > > That's something I discovered and yes, that's a DCL vulnerability > > that laid undiscovered in VMS for 33 years until I found it. >=20 > That S/W didn't become stale; it was always incorrect and unreliable. Yes, if & only if your design extraordinarily-wisely considered the entire = universe of axiom systems, not only now known, but knowable until the end o= f time in the far future. But practically speaking, for mere mortals/non-g= ods, such foresight is at least impractical if not impossible, so Simon Clu= bley is more correct in practice than you on this issue. Randy, hence the provability of anything in Ada (e.g., tasking in Ada2020) = is only as good as an explicitly enumerated inventory of axioms. The very = most awesome would be for Ada-for-the-21st-century to declare such axioms i= n the Ada source code (for source-code-requested Ada-compiler-based correct= ness proving). Almost as awesome would be for the ARM to declare such axio= ms in a declarative language other than English prose (so that they can be = parsed by compiler vendors when authoring/analyzing their compiler's source= code). Somewhat stinky but better than nothing would be for the ARG to ov= ertly declare such axioms in English prose in writing in the ARM. Living d= angerously would be for some members of the ARG to hold differing partial a= xiom systems mentally in their head while writing the ARM. Total failure i= s likely from no one ever attempting to enumerate any axioms on which (shak= y house-of-cards) (so-called-)provability is based.