Krishna Myneni <krishna.myneni@ccreweb.org> writes:
>On 3/2/24 10:08, Krishna Myneni wrote:
>> === Gforth example ===
>> : rt1 recurse ;  ok
>> rt1
>> *the terminal*:2:1: error: Return stack overflow
>> >>>rt1<<<
>> === end example ===
>>
>
>To be clear, if you try to fill up the fp or data stack, as with your
>rt1 example, kForth does give a segfault (and hence is susceptible to an
>exploit), while Gforth still gives the same error.

In Gforth on a Unix system, Unix produces a SIGSEGV when a stack runs
into a guard page. The signal handler then looks at the offending
address, and guesses that an access close to the bottom of a stack is
an underflow of that stack, and correspondingly for accesses close to
the top of a stack. This can be seen as follows:

With the gforth engine with the FP stack being empty:

fp@ 32769 - c@
*the terminal*:3:13: error: Floating-point stack overflow
fp@ 32769 - >>>c@<<<
fp@ 1+ c@
*the terminal*:4:8: error: Floating-point stack underflow
fp@ 1+ >>>c@<<<

- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: https://forth-standard.org/
EuroForth 2023: https://euro.theforth.net/2023

On 3/2/24 10:43, Anton Ertl wrote:
> Krishna Myneni <krishna.myneni@ccreweb.org> writes:
>> On 3/2/24 10:08, Krishna Myneni wrote:
>>> === Gforth example ===
>>> : rt1 recurse ;  ok
>>> rt1
>>> *the terminal*:2:1: error: Return stack overflow
>>> >>>rt1<<<
>>> === end example ===
>>>
>>
>> To be clear, if you try to fill up the fp or data stack, as with your
>> rt1 example, kForth does give a segfault (and hence is susceptible to an
>> exploit), while Gforth still gives the same error.
>
> In Gforth on a Unix system, Unix produces a SIGSEGV when a stack runs
> into a guard page. The signal handler then looks at the offending
> address, and guesses that an access close to the bottom of a stack is
> an underflow of that stack, and correspondingly for accesses close to
> the top of a stack. This can be seen as follows:
>
> With the gforth engine with the FP stack being empty:
>
> fp@ 32769 - c@
> *the terminal*:3:13: error: Floating-point stack overflow
> fp@ 32769 - >>>c@<<<
> fp@ 1+ c@
> *the terminal*:4:8: error: Floating-point stack underflow
> fp@ 1+ >>>c@<<<
>

Nice. The use of guard pages is something I need to look into to avoid
memory leaks or corruption for the stacks. Does this mean Gforth is
immune to arbitrary code execution attacks for the fp and data stack
overflow and underflow conditions?

--
Krishna

Krishna Myneni <krishna.myneni@ccreweb.org> writes:
>Does this mean Gforth is
>immune to arbitrary code execution attacks for the fp and data stack
>overflow and underflow conditions?

Technically, one might answer "yes", but there are stack depth
violations that don't result in a stack overflow or underflow, and
that can lead to arbitrary code execution in Gforth. A simple example
is:

: bla ." bla" ;

: foo >r ;

' bla >body foo \ prints "bla"

Essentially, there is far too few guardrails in Gforth for the guard
pages to provide significant safety. For Gforth they are just a
convenience feature.

However, the idea of Safe Forth is to eliminate all these other ways
towards arbitrary code execution, and in Safe Forth the guard pages
will close the hole that stack overflows and underflows would
otherwise leave open.

Note that guard pages require OS support; Gforth uses the mprotect()
system call (of modern (since ~1990) Unix systems) for that.

- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: https://forth-standard.org/
EuroForth 2023: https://euro.theforth.net/2023

dxf <dxforth@gmail.com> writes:
> It's good to have an application that works as planned but how does one
> that misbehaves translate to 'security risk'

If the misbehaviour is related to the program input, and the input is
supplied by an attacker, they will look for an input that breaks security.

> and how does 'memory-safe' prevent that?

"Prevent" is too strong a term, but it helps. A classic attack is when
you have a memory buffer on the stack, but accesses to it are not bounds
checked. That means the attacker can overwrite stuff on the stack after
the memory buffer, such as the procedure's return address. That means
the attacker can make the program jump to the location of their choice,
i.e. a location containing a security attack. See:

https://en.wikipedia.org/wiki/Return-oriented_programming

> That may be their belief (fancy word for hope) but do they have anything
> to back it up?

It's unclear what they mean, but it's certainly the case that studying
the historical corpus of CVE's tells us things about common types of
attacks. That tells us what areas need attention.

Regarding runtime checks: in C++, if you access an array as a[i], there
is no runtime check and thus there is a potential out-of-range memory
access. If you instead say a.at(i), there is a runtime check, so you
get the right result if the index is in range, but raise an exception
otherwise. What I've found in practice is that there is almost no
slowdown. I suspect that the memory access itself is slower than the
range check, even when it usually is within the cpu cache. So this says
runtime checks are usually worth the small cost.

You can compile in DEBUG/RELEASE mode, whereby runtime checks
are no longer included in RELEASE mode. But these are quasi
pre-mortem traps, just like guard pages - they do not make Forth
safer as a language, for that it would need a-priori error traps.

An example:
: TE1 -1 dup c! ;

TE1 contains two errors: -1 is not a char and -1 is not a permitted
memory address. It must be possible to catch these during compilation.

Even the so vulnerable language C has assert macros for compiling
in DEBUG mode. In Forth, you have to create asserts yourself.

Paul Rubin <no.email@nospam.invalid> writes:
>It's unclear what they mean, but it's certainly the case that studying
>the historical corpus of CVE's tells us things about common types of
>attacks. That tells us what areas need attention.

My impression from reading articles like
<https://lwn.net/Articles/961978/> and the discussions after them is
that in recent years CVEs have become a metric for evaluating security
researchers, and, like any other metric, are therefore gamed. So
these days a statistic about CVEs tells us only what kind of bugs
which are assumed to be vulnerabilities are most often found by those
researchers.

>What I've found in practice is that there is almost no
>slowdown. I suspect that the memory access itself is slower than the
>range check, even when it usually is within the cpu cache.

On a modern OoO processor, if the program is dependence-bound rather
than resource-bound, the instructions for the range check cost very
little, because they do not add to the dependence chains in the usual
case (when the access is in range).

- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: https://forth-standard.org/
EuroForth 2023: https://euro.theforth.net/2023

minforth@gmx.net (minforth) writes:
>In Forth, you have to create asserts yourself.

Or you can use Gforth, which has them since at least gforth-0.2
(released 1996). See
<https://gforth.org/manual/Assertions.html#index-assert_0028>.

- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: https://forth-standard.org/
EuroForth 2023: https://euro.theforth.net/2023

On 3/2/24 10:43, Anton Ertl wrote:
> Krishna Myneni <krishna.myneni@ccreweb.org> writes:
>> On 3/2/24 10:08, Krishna Myneni wrote:
>>> === Gforth example ===
>>> : rt1 recurse ;  ok
>>> rt1
>>> *the terminal*:2:1: error: Return stack overflow
>>> >>>rt1<<<
>>> === end example ===
>>>
>>
>> To be clear, if you try to fill up the fp or data stack, as with your
>> rt1 example, kForth does give a segfault (and hence is susceptible to an
>> exploit), while Gforth still gives the same error.
>
> In Gforth on a Unix system, Unix produces a SIGSEGV when a stack runs
> into a guard page. The signal handler then looks at the offending
> address, and guesses that an access close to the bottom of a stack is
> an underflow of that stack, and correspondingly for accesses close to
> the top of a stack. This can be seen as follows:
>
> With the gforth engine with the FP stack being empty:
>
> fp@ 32769 - c@
> *the terminal*:3:13: error: Floating-point stack overflow
> fp@ 32769 - >>>c@<<<
> fp@ 1+ c@
> *the terminal*:4:8: error: Floating-point stack underflow
> fp@ 1+ >>>c@<<<
>

In the version of Gforth which I have (0.7.9_20220120),

fp@ 32769 - c@
*the terminal*:5:13: error: Floating-point stack overflow
fp@ 32769 - >>>c@<<<

However,

fp@ 65536 - c@ ok 1

and, worse,

1 fp@ 65536 - c! ok

So the guard pages are not a solution to pointer arithmetic bugs with
the stack pointers.

To make stack access memory safe, there has to be bounds checks on
reading and writing from/to stacks. This suggests that stacks should be
arrays and stack operations always involve array read/write from arrays
with enforced bounds checking e.g. something like

: DUP STACK[ tos ]@ ; \ TOS returns an index to the top of the stack
: OVER STACK[ tos 1+ ]@ ;

etc. and ]@ and ]! performs bounds checks.

I haven't yet looked at your paper on SafeForth.

--
Krishna

On 3/03/2024 2:39 am, minforth wrote:
> Harden these without runtime checks:
> : RT1 2 3e recurse ;
> : RT2 drop fdrop recurse ;

Garbage in, garbage out.

What do I use while developing a recursive function: ?STACK.
Chances of needing it in a completed application are about
the same as winning the lottery.

On 2/03/2024 8:47 pm, albert@spenarnc.xs4all.nl wrote:
> In article <65e2c0f3$1@news.ausics.net>, dxf <dxforth@gmail.com> wrote:
>> On 2/03/2024 5:17 am, Paul Rubin wrote:
>>> anton@mips.complang.tuwien.ac.at (Anton Ertl) writes:
>>>>> of the renewed recent push for use of memory-safe languages.
>>>> Which "renewed recent push" do you mean?
>>>
>>>
>> https://www.tomshardware.com/software/security-software/white-house-urges-developers-to-avoid-c-and-c-use-memory-safe-programming-languages
>>>
>>>
>> https://www.whitehouse.gov/oncd/briefing-room/2024/02/26/press-release-technical-report/
>>
>> It's good to have an application that works as planned but how does one
>> that misbehaves translate to 'security risk' and how does 'memory-safe'
>> prevent that?
>>
>> "ONCD has the belief that better metrics enable technology providers to
>> better plan, anticipate, and mitigate vulnerabilities before they become
>> a problem."
>>
>> That may be their belief (fancy word for hope) but do they have anything
>> to back it up?
>>
>
> Most Forthers have a blind spot what safe means.
> I grew up with algol60. The only errors you encountered were
> array index errors, and memory exhausted. Index errors showed what array
> the index, and a call tree. Memory exhausted indicates that you have
> infinite recursion.
> On the other hand FORTRAN programs showed an hex address and a dump of
> the internal registers.

Blind is believing one doesn't have to think because the system has one's
back. Forth is brutal in dispelling any such notions.

One of the criteria for 8th was security -- among other things, making
it very difficult to do unsafe memory operations. Within 8th itself you
can't; but of course, with the FFI anything is possible.

On 01/03/2024 17:54, Krishna Myneni wrote:
> I'm wondering what the CS Forth users and Forth systems developers make
> of the renewed recent push for use of memory-safe languages. Certainly
> Forth can add the type of contractual safety requirements e.g.,
> implementing bounds checking, of a "memory-safe language". Do we need to
> work on libraries for these provisions?
>
> Opinions?
>
> --
> Krishna Myneni
>

Krishna Myneni <krishna.myneni@ccreweb.org> writes:
>On 3/2/24 10:43, Anton Ertl wrote:
>> With the gforth engine with the FP stack being empty:
>>
>> fp@ 32769 - c@
>> *the terminal*:3:13: error: Floating-point stack overflow
>> fp@ 32769 - >>>c@<<<
>> fp@ 1+ c@
>> *the terminal*:4:8: error: Floating-point stack underflow
>> fp@ 1+ >>>c@<<<
>>
>
>In the version of Gforth which I have (0.7.9_20220120),
>
>fp@ 32769 - c@
>*the terminal*:5:13: error: Floating-point stack overflow
>fp@ 32769 - >>>c@<<<
>
>However,
>
>fp@ 65536 - c@ ok 1
>
>and, worse,
>
>1 fp@ 65536 - c! ok
>
>So the guard pages are not a solution to pointer arithmetic bugs with
>the stack pointers.

Yes, that is not their intention and not the intention of these
examples. The intention of these examples is to show that any memory
access will be interpreted as a stack underflow or overflow if it is
to a certain range of addresses.

A more serious issue is that, as implemented in Gforth (in particular,
gforth-fast), stack underflows can be undetected in some cases: On
Gforth on an AMD64 system, with the data stack being empty:

600 pick ok 1

On gforth-fast, with the data stack being empty:

: foo 600 0 ?do nip loop cr . ; foo
0
*the terminal*:1:33: error: Stack underflow
: foo 600 0 ?do nip loop cr . ; >>>foo<<<
Backtrace:
kernel/basics.fs:312:27: 0 $7F30E3BDFE10 throw

Note that FOO actually performs the "cr .", so the stack underflow is
not detected by an access to the the guard page. Instead, the text
interpreter checks the stack pointer and reports a stack underflow.
The non-detection of the stack underflow is because NIP is implemented
as:

$7F30E3C72C90 nip 1->1
7F30E3917557: add r13,$08 #update sp

With the gforth engine, a similar scenario (involving DROP) is avoided
because in this engine DROP loads the value being dropped exactly to
trigger stack underflow reports where they happen:

$7F55EBFA6C98 drop 0->0
7F55EBAC51C0: mov $50[r13],r15 #save ip (for accurate backtraces)
7F55EBAC51C4: add r15,$08 #update ip
7F55EBAC51C8: mov rax,[r14] #load dropped value
7F55EBAC51CB: add r14,$08 #update sp

Neither the deep PICK nor the loop that just NIPs or DROPs occur in
practice.

The motivation for the otherwise unnecessary load in DROP (in gforth)
is code sequences like

drop 1

in cases where the stack is empty. The load in DROP results in
detecting the stack underflow at the DROP rather than at the "1".
Reporting a stack underflow at an operation that just pushes can
produce a WTF moment in the programmer; the gforth engine exists to
make debugging easier, and that includes avoiding such moments.

>To make stack access memory safe, there has to be bounds checks on
>reading and writing from/to stacks. This suggests that stacks should be
>arrays and stack operations always involve array read/write from arrays
>with enforced bounds checking e.g. something like
>
>: DUP STACK[ tos ]@ ; \ TOS returns an index to the top of the stack
>: OVER STACK[ tos 1+ ]@ ;
>
>etc. and ]@ and ]! performs bounds checks.

With guard pages, that's not necessary. The normal bounded-depth
stack accesses (of words like 2DROP or 2OVER) are sure to hit the
guard pages if the stack is out-of-bounds; you may want to perform an
otherwise unnecessary load on words like NIP, DROP, 2DROP etc. that do
not otherwise use (and thus load) the stack values that they consume,
but that's much cheaper than putting bounds checks on every stack
access. For unbounded stack-access words like PICK, a bounds check is
appropriate.

- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: https://forth-standard.org/
EuroForth 2023: https://euro.theforth.net/2023

You can run around in circles here, the basic problem is that there is
no formal specification for what a safe programming language is.
Analyses on the subject are dominated by the following: Memory errors,
type errors, range errors, race condition errors.

In order to develop Forth more in this direction, we would first need
a specification on "Hardened Forth" that is dedicated to these error
areas - and also marks UBs with defined exception codes. Ideally
accompanied by a test suite so that every Forth system developer can
check their own system.

On 3/3/24 01:25, Anton Ertl wrote:
> Krishna Myneni <krishna.myneni@ccreweb.org> writes:
>> On 3/2/24 10:43, Anton Ertl wrote:
>>> With the gforth engine with the FP stack being empty:
>>>
>>> fp@ 32769 - c@
>>> *the terminal*:3:13: error: Floating-point stack overflow
>>> fp@ 32769 - >>>c@<<<
>>> fp@ 1+ c@
>>> *the terminal*:4:8: error: Floating-point stack underflow
>>> fp@ 1+ >>>c@<<<
>>>
>>
>> In the version of Gforth which I have (0.7.9_20220120),
>>
>> fp@ 32769 - c@
>> *the terminal*:5:13: error: Floating-point stack overflow
>> fp@ 32769 - >>>c@<<<
>>
>> However,
>>
>> fp@ 65536 - c@ ok 1
>>
>> and, worse,
>>
>> 1 fp@ 65536 - c! ok
>>
>> So the guard pages are not a solution to pointer arithmetic bugs with
>> the stack pointers.
>
> Yes, that is not their intention and not the intention of these
> examples. The intention of these examples is to show that any memory
> access will be interpreted as a stack underflow or overflow if it is
> to a certain range of addresses.
>
> A more serious issue is that, as implemented in Gforth (in particular,
> gforth-fast), stack underflows can be undetected in some cases: On
> Gforth on an AMD64 system, with the data stack being empty:
>
> 600 pick ok 1
>
> On gforth-fast, with the data stack being empty:
>
> : foo 600 0 ?do nip loop cr . ; foo
> 0
> *the terminal*:1:33: error: Stack underflow
> : foo 600 0 ?do nip loop cr . ; >>>foo<<<
> Backtrace:
> kernel/basics.fs:312:27: 0 $7F30E3BDFE10 throw
>
> Note that FOO actually performs the "cr .", so the stack underflow is
> not detected by an access to the the guard page. Instead, the text
> interpreter checks the stack pointer and reports a stack underflow.
> The non-detection of the stack underflow is because NIP is implemented
> as:
>
> $7F30E3C72C90 nip 1->1
> 7F30E3917557: add r13,$08 #update sp
>
> With the gforth engine, a similar scenario (involving DROP) is avoided
> because in this engine DROP loads the value being dropped exactly to
> trigger stack underflow reports where they happen:
>
> $7F55EBFA6C98 drop 0->0
> 7F55EBAC51C0: mov $50[r13],r15 #save ip (for accurate backtraces)
> 7F55EBAC51C4: add r15,$08 #update ip
> 7F55EBAC51C8: mov rax,[r14] #load dropped value
> 7F55EBAC51CB: add r14,$08 #update sp
>
> Neither the deep PICK nor the loop that just NIPs or DROPs occur in
> practice.
>
> The motivation for the otherwise unnecessary load in DROP (in gforth)
> is code sequences like
>
> drop 1
>
> in cases where the stack is empty. The load in DROP results in
> detecting the stack underflow at the DROP rather than at the "1".
> Reporting a stack underflow at an operation that just pushes can
> produce a WTF moment in the programmer; the gforth engine exists to
> make debugging easier, and that includes avoiding such moments.
>
>> To make stack access memory safe, there has to be bounds checks on
>> reading and writing from/to stacks. This suggests that stacks should be
>> arrays and stack operations always involve array read/write from arrays
>> with enforced bounds checking e.g. something like
>>
>> : DUP STACK[ tos ]@ ; \ TOS returns an index to the top of the stack
>> : OVER STACK[ tos 1+ ]@ ;
>>
>> etc. and ]@ and ]! performs bounds checks.
>
> With guard pages, that's not necessary. The normal bounded-depth
> stack accesses (of words like 2DROP or 2OVER) are sure to hit the
> guard pages if the stack is out-of-bounds; you may want to perform an
> otherwise unnecessary load on words like NIP, DROP, 2DROP etc. that do
> not otherwise use (and thus load) the stack values that they consume,
> but that's much cheaper than putting bounds checks on every stack
> access. For unbounded stack-access words like PICK, a bounds check is
> appropriate.
>

That's a pretty good approach, to use guard pages for stack access words
which are guaranteed to trigger a signal, and use bounds checking for
the remaining ones.

The intent of the stack array access was to avoid stack pointer
arithmetic altogether. Stack array access words provide a safe alternate
to doing stack pointer arithmetic in Forth code. Pointer arithmetic
appears to be the source of a lot of memory safety problems.

--
Krishna

On 3/2/24 13:47, minforth wrote:
> You can compile in DEBUG/RELEASE mode, whereby runtime checks
> are no longer included in RELEASE mode. But these are quasi
> pre-mortem traps, just like guard pages - they do not make Forth
> safer as a language, for that it would need a-priori error traps.
>
> An example:
>
> : TE1 -1 dup c! ;
>
> TE1 contains two errors: -1 is not a char and -1 is not a permitted
> memory address. It must be possible to catch these during compilation.

kForth, from its beginning, would never execute the C! in your example:

Ready!
: TE1 -1 dup c! ;
ok
TE1
Line 2: VM Error(-256): Not data type ADDR
TE1

It performs run-time type checking for address arguments, at about 15%
cost in speed for most benchmarks.

--
Krishna

On 3/3/24 02:21, minforth wrote:
> You can run around in circles here, the basic problem is that there is
> no formal specification for what a safe programming language is.
> Analyses on the subject are dominated by the following: Memory errors,
> type errors, range errors, race condition errors.
>
> In order to develop Forth more in this direction, we would first need
> a specification on "Hardened Forth" that is dedicated to these error
> areas - and also marks UBs with defined exception codes. Ideally
> accompanied by a test suite so that every Forth system developer can
> check their own system.

I'm not smart enough for a top down approach to this problem. The Forth
approach is one that I can take though. Start with small well-defined
problems, and try to find solutions for those. Build up a bigger picture
from those solutions.

--
Krishna

That's patchwork, but if it is sufficient for a program,
good for the program. As for language safety....

For instance, I wouldn't define how to react on
0 BASE !
that could lead to a plethora of system-dependent crashes.
Or on
-1. 3 UM/MOD
probably throw exception code -11 for result out of range
even when 'range' is undeclared or only implicit.

OTOH I doubt that there is any demand for a paranoia Forth
with safety belts and suspenders and alarm whistles.

Krishna Myneni <krishna.myneni@ccreweb.org> writes:
>The intent of the stack array access was to avoid stack pointer
>arithmetic altogether. Stack array access words provide a safe alternate
>to doing stack pointer arithmetic in Forth code. Pointer arithmetic
>appears to be the source of a lot of memory safety problems.

At the machine level and the standard Forth level, every array access
performs address arithmetics. Given that standard Forth does not
expose the implementation of the stacks, there is no need to use some
specific implementation for them. One may wonder, though, if using 4
stacks with guard pages around them (i.e., at least 9 pages per task,
set up with 6 system calls) is too expensive for multi-tasking; I
think Gforth currently only does it for the main task.

There are architectures (in particular, the 80286) that provide
hardware support for treating stretches of memory as segments with
bounds checking, and the idea probably was that every array becomes a
segment (not sure about structures; the 80286 supports only 8192
segments, which seems a little low if every struture needs a segment),
but anyway, using segments was too cumbersome, slow and limited, so
they have been let slide by the wayside in the descendents of the
architecture (IA-32, AMD64).

In any case, yes, in Safe Forth there are no addresses at the language
level. You have objects with value-flavoured fields, and arrays with
indexed-fetch and indexed-store words. But in the implementation of
Safe Forth, there will certainly be address arithmetics.

- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: https://forth-standard.org/
EuroForth 2023: https://euro.theforth.net/2023

minforth@gmx.net (minforth) writes:
>You can run around in circles here, the basic problem is that there is
>no formal specification for what a safe programming language is.

It was certainly an interesting aspect of my work on Safe Forth that I
first had to understand better what memory safety is; I had the "I
know it when I see it" kind of understanding, but that was not enough.
But I succeeded in understanding it better, and you can read the paper
if you want to know more about it.

>Analyses on the subject are dominated by the following: Memory errors,
>type errors, range errors, race condition errors.

Safe Forth only tries to solve memory errors. That makes it necessary
to deal with some type errors and some range errors, but not all of
them, and there are no ambitions at the moment to harden Safe Forth
more against those. My idea on how to perform multitasking in Safe
Forth does not provide shared memory, so there are no race conditions.

>In order to develop Forth more in this direction, we would first need
>a specification on "Hardened Forth" that is dedicated to these error
>areas - and also marks UBs with defined exception codes.

I know "UB" from the C language lawyers. They love the concept of
"undefined behaviour" so much that they have created a 2-letter
acronym for it. A safe language does not have undefined behaviour,
and if you define the behaviour on some kind of condition to perform
an exception, that behaviour is certainly not undefined.

- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: https://forth-standard.org/
EuroForth 2023: https://euro.theforth.net/2023

minforth@gmx.net (minforth) writes:
> You can run around in circles here, the basic problem is that there is
> no formal specification for what a safe programming language is.

From https://en.wikipedia.org/wiki/Ada_(programming_language)#History :

HOLWG crafted the Steelman language requirements, a series of
documents stating the requirements they felt a programming language
should satisfy. Many existing languages were formally reviewed, but
the team concluded in 1977 that no existing language met the
specifications.

They put out for proposals for a new language to be designed. The
eventual winner was Ada, but that choice came with some controversy at
the time. There were competing proposals that some people felt were
less bloated and still fulfilled the intended goals.

Don't look elsewhere for UBs, the Forth Standard is shock full of "ambiguous conditions"

Paul Rubin wrote:
> They put out for proposals for a new language to be designed. The
> eventual winner was Ada, but that choice came with some controversy at
> the time. There were competing proposals that some people felt were
> less bloated and still fulfilled the intended goals.

Misra-C is an example. There is no language specification, but quite a
number of rules against which a C program can be checked.

minforth@gmx.net (minforth) writes:
> Misra-C is an example. There is no language specification, but quite a
> number of rules against which a C program can be checked.

Misra-C has some sensible rules, but it's still C, which comes nowhere
near meeting the requirements that the working group (that chose Ada)
was looking for. Maybe some subset of C++ could have done done it.
C doesn't have nearly enough type safety.

On 3/3/24 10:08, minforth wrote:
> That's patchwork, but if it is sufficient for a program,
> good for the program. As for language safety....
>
....
> OTOH I doubt that there is any demand for a paranoia Forth
> with safety belts and suspenders and alarm whistles.

Perhaps not, but I wrote my Forth system to provide some hand-holding,
primarily for my own needs. My expectation is that the demand for Forth
systems which don't address safety concerns will rapidly drop to zero.

--
Krishna

On 3/03/2024 4:54 pm, Ron AARON wrote:
> One of the criteria for 8th was security -- among other things, making it very difficult to do unsafe memory operations.

Has it paid off - by which I mean completed apps that out of the blue access
invalid memory? I'm curious as to what exactly is behind the high rate of
'memory errors' that govt et al is reporting because in my limited experience
programming in Forth, I'm just not seeing any. I wonder if it has something
to do with the practices employed in those other languages - such as the use
of third-party libraries which programmers use essentially on faith.