Re: How to get Ada to ?cross the chasm??

["Dan'l Miller" <optikos@verizon.net>]

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:
> > 
> > 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.
> 
> 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 worst hold vague rules of thumb as a perceived reference model of how the underlying machine is thought to work; Nancy Leveson goes into the necessity of this obfuscating-the-details mental model in her book _Safeware: System safety and computers_).

For example, if mandatory Harvard architectures* were the norm when the operating system's source code was authored (e.g., ARM), then the operating system is ported to a von Neumann architecture** (e.g., Intel, AMD with ), then suddenly the operating system's underlying axiom system changed beneath it at the hardware level.  Suddenly, the operating system is oblivious to the need to inhibit data from being executable machine instructions.  This is an example of Simon Clubley's “probing for security issues in new ways”.  An extant example of the reverse direction effectively occurred when Intel & AMD & ARM & POWER & Alpha & SPARC all added their various-named analogues of NX bit to emulate Harvard architecture protections on a von Neumann architecture.  Then suddenly operating systems had the security axiom system shifted underneath them to properly securely enact a de facto Harvard architecture when  they had insecurely assumed von Neumann up until 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:
> > 
> > http://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2017-17482
> > 
> > That's something I discovered and yes, that's a DCL vulnerability
> > that laid undiscovered in VMS for 33 years until I found it.
> 
> 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 of time in the far future.  But practically speaking, for mere mortals/non-gods, such foresight is at least impractical if not impossible, so Simon Clubley 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 in the Ada source code (for source-code-requested Ada-compiler-based correctness proving).  Almost as awesome would be for the ARM to declare such axioms 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 overtly declare such axioms in English prose in writing in the ARM.  Living dangerously would be for some members of the ARG to hold differing partial axiom systems mentally in their head while writing the ARM.  Total failure is likely from no one ever attempting to enumerate any axioms on which (shaky house-of-cards) (so-called-)provability is based.