Yet another leak in the sinking ship of @safe

[H. S. Teoh via Digitalmars-d]

On Thu, Feb 18, 2016 at 08:23:24PM +0100, Timon Gehr via Digitalmars-d wrote:
> On 18.02.2016 19:41, H. S. Teoh via Digitalmars-d wrote:
[...]
> >	void breakSafety(void[] data) @safe
> >	{
> >		union U {
> >			void[] d;
> >			int[] arr;
> >		}
> >		U u;
> >		u.d = data;
> >		u.arr[0] = 0xFF; // kaboom
> >	}
> >...
> 
> That's in essence just a different way to cast void[] to int[].
> Steven's example disproves my previous claim though. Still, I don't
> think the conversion is the problem. It's the mutation of memory
> without type information.

Fair enough.  But mutating memory *with* type information isn't
necessarily safer either:

	void fun(int*[] intPtrs) {
		union U {
			int*[] ptrs;
			long[] longs;
		}
		U u;
		u.ptrs = intPtrs;
		u.longs[0] = 12345; // oops
	}

Basically, when it comes to @safe, one of the intrinsic requirements is
that arbitrary values must not be reinterpreted as pointers. In a sense,
it doesn't matter how you get there -- whether by implicit cast to
void[], or by unions, or whatever -- as soon as there is a way to
reinterpret an arbitrary value as a pointer, @safe is broken. The
arbitrary can be another pointer, and may even be a pointer to a type
with a compatible binary representation, but the point remains. For
example:

	void safeFunc() @safe { ... }
	void unsafeFunc() @system { ... }

	union FuncPtrs {
		void function() @safe fun1;
		void function() @system fun2;
	}
	FuncPtrs ptrs;
	ptrs.fun1 = &unsafeFunc();
	ptrs.fun2();			// oops

>From the POV of binary representation, both fun1 and fun2 are
essentially the same -- they are just function pointers: 32-bit or
64-bit addresses of some executable code. However, the breakage here is
caused by reinterpreting a pointer to a @system function as a pointer to
a @safe function.  At no time do we lose type information, but as soon
as we have reintepretation of something as a pointer, @safe is out the
window.


[...]
> >>>2) To add salt to the wound, though, blatantly casting void[] to
> >>>T[] is allowed in @safe code, thus, readData() can even get away
> >>>with claiming to be @safe, when in fact it is anything but.
> >>>
> >>>	https://issues.dlang.org/show_bug.cgi?id=15672
> >>
> >>This is the culprit.
> >
> >It's only one of many culprits. As long as there is any way around
> >@safe, the entire system of guarantees breaks down.
> >
> >
> 
> If you want to verify guarantees, @safe should be specified by
> inclusion and ideally, type safety should be proved formally (after
> applying a few fixes).
> This first requires a formal language semantics.
> That's already a lot of effort, and after that you still don't have a
> verified implementation.

I'm not sure how feasible it is to do a formal proof with the current
dmd code, since you'd have to freeze it, and as soon as the next PR is
merged, the proof is potentially invalidated.

However, a good start is to make *everything* in the language @system by
default, and then have a whitelist of things that are @safe. Currently,
our implementation is to assume @safety by default and then add things
to a @system blacklist as we discover them.  This is the wrong approach,
since we don't know what loopholes currently exist that can be
exploited, and the number of combinations of language features is far
too large for us to be ever sure that we've plugged all the holes. It's
better to start conservatively by assuming everything is @system, and as
people find more valid use cases that ought to be @safe, those can be
added to the whitelist after careful vetting.  This is essentially the
idea behind:

	https://issues.dlang.org/show_bug.cgi?id=15672


T

-- 
You have to expect the unexpected. -- RL