i feel that the grammar of a programming language is among the least appropriate of all possible facets of its behavior to start off with.

[miss_rodent@girlcock.club]

@hipsterelectron ... if *C* is that complicated, the higher level languages must all be just completely fucked, then, by this standard.

[hipsterelectron@circumstances.run]

https://trustworthy.systems/publications/papers/Tuch%3Aphd.pdf

this one is hosted on the seL4 site

Systems impose on languages many abstraction breaking requirements

"systems" lmao

and are not usually considered amenable to implementation in higher-level languages like Java and ML.

yeah cause the JVM abstract machine is specifically built to be this fucked up carnival ride. you could do it if you specifically forked the JVM. hate this lack of precision from ppl who are so loud about "formalism"

For example, zero-copy I/O and address translation are crucial features

zero-copy IO and address translation are extremely different things. zero-copy IO doesn't even make sense in ring 0 and is not in fact a "crucial feature". it's not even a language feature!

and programmers demand the freedom to control data structure layout [87],

you can "control data structure layout" in any language that lets you address bytes which i think is literally all of them. C struct layout is actually rly annoying because you can't let the compiler help you at all

in particular when optimising the cache and TLB footprint that is typically opaque in such languages.

those aren't your data structures those are the CPU's and that's ring 0 again, not a language feature

Inside the research community there are recent promising efforts at harnessing the gains of the last three decades of programming language research [8, 22, 29, 37, 46, 68, 89],

guy who knows nothing about anything he just said: "i represent the 'research community' and we will exterminate your kind"

with an emphasis on types and static checking, when implementing systems.

this guy grew into the rust evangelism strike force

However, these advances are yet to be popularised in industry

guy who thinks "systems" are an industry-specific thing

and still face enormous scepticism from systems implementors who are highly obsessed
with efficiency, sometimes to the extreme where clock cycles are the metric of choice.

this fucking guy!!!!! clock cycles can actually be counted reliably lmao. THIS is what seL4 is standing behind

[hipsterelectron@circumstances.run]

Even today, it is easy to violate the C type system by its cast mechanism and through address arithmetic.

guy who thinks C's type system is being violated through casting and address arithmetic. you know those have concrete semantics right

The programmer is given, intentionally, access to low-level bit and byte representations of values in memory.

again, that's literally every language

There are no checks on array bounds when indexing — this would violate C’s design philosophy.

the guy who is telling you with a straight face that he totally formalized C semantics for high-assurance ring 0 scenarios is now telling you he finds the language detestable

[hipsterelectron@circumstances.run]

god it would be so cool if rust gave a shit about correctness

[jab01701mid@mastodon.social]

@hipsterelectron Kind of reminds me of "Proven in Use" defense in automotive, SIL-levels.

Because a certain design has worked for 50 years, it's taken to be correct. Something like that. Now we are down to a few weeks or a product ?

"The requirements of these schemes can be met either by establishing a rigorous development process, or by establishing that the device has sufficient operating history to argue that it has been proven in use."

Safety integrity level - Wikipedia

(en.wikipedia.org)

[hipsterelectron@circumstances.run]

C does not have garbage collection and the programmer is responsible for allocation and deallocation of memory through library calls.

"library calls" why would you declare that you don't know the semantics at all

A systems implementor may even develop his or her own memory allocator that replaces this already low-level interface, enabling direct management of the physical memory in a system.

THIS IS THE GUY WHO IS CLAIMING HE KNOWS WHAT SEMANTICS ARE!

[hipsterelectron@circumstances.run]

Unfortunately, systems code is by no means strictly conforming and we could say by definition requires the ability to violate the standard’s strict rules on how memory can be accessed.

i am literally going to go find the C standard right now because the model of globally addressable memory space is i'm pretty sure the one thing that's not violated

[natty@astolfo.social]

@hipsterelectron@circumstances.run to be fair there's defined semantics and then there's the "defined semantics"

[somebody@tech.lgbt]

@hipsterelectron really concerning and unsafe that the average oven gives you number level access to the thermostat.

[hipsterelectron@circumstances.run]

like personally i think someone (not this guy) could make a pretty effective case for having correctly represented the semantics of C in ring 0 in a theorem prover even if they didn't link it to precise lines of C code through a model in the compiler,,,,

but if i was ever gonna say anything like "high-assurance" or "secure" i would actually do the work to link my semantic model to the one in the compiler and the CPU/RAM. and i would bully c standards people into accepting it

[hipsterelectron@circumstances.run]

As a result, when describing type safety with respect to a C program in this thesis, we refer to a looser notion,

bruh. don't say things like that

where we may require expressions that designate a memory object to have a type corresponding to the expected value stored in memory.

he should have said "type" to clarify that that was gonna be the subject of debate. but this guy represents the "research community" so i bet he thinks his type is Correct

Program fragments can be type-safe if all their expressions have this property and later we formalise what is meant by the expected value’s type.

"type-safe". usually in cryptography we don't invoke generic informal terminology when we want people to take us seriously

[hipsterelectron@circumstances.run]

Memory management code tracks the free memory that can be allocated and also sometimes the memory that has been allocated.

he just keeps going??????? here i'll translate:

• "the free memory that can be allocated": sometimes non-micro kernels like linux maintain free lists of unmapped physical pages so that moving the sbrk can be made very fast if not completely atomic
• "and also sometimes the memory that has been allocated": i suspect this is referring to a process's virtual address mapping, but maybe it's referring to an in-kernel allocator

[hipsterelectron@circumstances.run]

This is commonly done through pointer-linked data structures,

why are we still saying "pointer" when we're in ring 0???? that's a physical address buddy

and this use of what are also called mutable inductively-defined data structures

no citation here is so disrespectful lmao

is the cause of a great degree of the difficulty in reasoning about such code formally.

i'm sorry you're having difficulty maybe it's time to give it up???

[hipsterelectron@circumstances.run]

This difficulty, a direct consequence of the use of indirection,

how are you still negging the reader like this

can be broken down as the aliasing [14] and frame [61] problems.

oh my GOD!!!!! ok so these fucking citations my god

[14] this is literally about virtual memory conforming to the C standard https://eis.mdx.ac.uk/staffpages/r_bornat/papers/MPC2000.pdf

The final difficulty is the complexity of the proofs: not only do we have to reason formally about sets, sequences, graphs and trees, we
have to make sure that the locality of assignment operations is reflected in the treatment of assertions about the heap.

EVEN THAT PAPER'S AUTHOR IS TELLING HIM TO DO HIS FUCKING JOB LOL

For all of these reasons, Hoare logic isn’t widely used to verify pointer programs. Yet most low-level and all object-oriented programs use heap pointers freely. If we wish to prove properties of the kind of programs that actually get written and used, we shall have to deal with pointer programs on a regular basis.

[hipsterelectron@circumstances.run]

literally nothing will prepare you for [61]

[hipsterelectron@circumstances.run]

[61] McCarthy and P. Hayes. Some philosophical problems from the
standpoint of artificial intelligence. In D. Michie and B. Meltzer, editors,
Machine Intelligence 4, pages 463–502. Edinburgh University Press,
1969.

[dalias@hachyderm.io]

@hipsterelectron Ring 0 uses the MMU. Kernel setting up MMU to map physical memory directly is an implementation choice, not something inherent to being a kernel/ring0.

A good kernel wouldn't do that.

[hipsterelectron@circumstances.run]

only possible alternative is he mistyped the reference address making a crucial point in his own phd thesis

[62] F. Mehta and T. Nipkow. Proving pointer programs in higher-order
logic. Information and Computation, 199(1-2):200–227, 2005.

and yes, it still assumes the heap. even though if you're managing physical memory. you do not have a heap

[hipsterelectron@circumstances.run]

god fuck and even this example is literally impossible

For an example of aliasing, consider a program with two pointer variables int * p and int * q and the following triple:

{| True |} ∗p = 37 ; ∗q = 42 ; {| ∗p = ? |}

not only has he just said "triple" without a citation like that's a well-known thing, this is the problem with it:

We are unable to ascertain the value pointed to by p as it may refer to the same location as q.

so you're telling me this C code:

int * p;
int * q;
*p = 37;
*q = 42;

demonstrates a classic aliasing problem....................does this guy even know about restrict or the concept of Undefined Behavior

[hipsterelectron@circumstances.run]

turns out a "hoare triple" is the fuckboy term for "precondition and postcondition" when you think you're the first to ever create an abstract machine for the C programming language

he never cites anything about a Hoare triple either

Hoare triples, where a block of code is preceded by a pre-condition and followed by a post-condition, have already appeared in §1.1.1.

he did just refer you, with a hyperlinked section heading, to the line above where he just says "triple"