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.
-
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 really concerning and unsafe that the average oven gives you number level access to the thermostat.
-
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
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
-
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
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
-
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
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
-
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
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???
-
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???
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.
-
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.
literally nothing will prepare you for [61]
-
literally nothing will prepare you for [61]
[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. -
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 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.
-
[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.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
-
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
god fuck and even this example is literally impossible
For an example of aliasing, consider a program with two pointer variables
int * pandint * qand 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
pas it may refer to the same location asq.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
restrictor the concept of Undefined Behavior -
god fuck and even this example is literally impossible
For an example of aliasing, consider a program with two pointer variables
int * pandint * qand 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
pas it may refer to the same location asq.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
restrictor the concept of Undefined Behaviorturns 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"
-
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"
The aliasing problem is much worse for inductively-defined data structures, where it is possible that structural invariants can be violated, and where we need more sophisticated recursive predicates to stipulate aliasing conditions.
this problem is so bad he has no example
These predicates appear in specifications, invariants and proofs, and their discovery is often a time consuming trial-and-error process.
sorry that you hate your job?
The aliasing situation becomes untenable when code is type-unsafe and we are forced to seek improved methods.
if the C compiler can unambiguously interpret it then maybe the C compiler is a better proof framework than isabelle/HOL
If instead we had a variable
float * p:{| True |} ∗p = 3 .14 ; ∗q = 42 ; {| ∗p = ? |}then not only do we have to consider aliasing between pointers of different types, but also the potential for p to be pointing inside the encoding of
∗qand vice versa.i don't know what language you're verifying but C has semantics here
We talk about this phenomenon as inter-type aliasing.
who's we
-
The aliasing problem is much worse for inductively-defined data structures, where it is possible that structural invariants can be violated, and where we need more sophisticated recursive predicates to stipulate aliasing conditions.
this problem is so bad he has no example
These predicates appear in specifications, invariants and proofs, and their discovery is often a time consuming trial-and-error process.
sorry that you hate your job?
The aliasing situation becomes untenable when code is type-unsafe and we are forced to seek improved methods.
if the C compiler can unambiguously interpret it then maybe the C compiler is a better proof framework than isabelle/HOL
If instead we had a variable
float * p:{| True |} ∗p = 3 .14 ; ∗q = 42 ; {| ∗p = ? |}then not only do we have to consider aliasing between pointers of different types, but also the potential for p to be pointing inside the encoding of
∗qand vice versa.i don't know what language you're verifying but C has semantics here
We talk about this phenomenon as inter-type aliasing.
who's we
While specifications may mention some state that is affected by the intended behaviour of a program, it is hard to capture the state that is not changed.
literally a nonsense sentence
In the above example, a client verification that also dereferences a pointer
r, not mentioned in the specification, has no information on its value after execution of the code fragment.meaningless
This limits reusability and hence scalability of verifications.
the C compiler is a better proof framework than isabelle/HOL
-
While specifications may mention some state that is affected by the intended behaviour of a program, it is hard to capture the state that is not changed.
literally a nonsense sentence
In the above example, a client verification that also dereferences a pointer
r, not mentioned in the specification, has no information on its value after execution of the code fragment.meaningless
This limits reusability and hence scalability of verifications.
the C compiler is a better proof framework than isabelle/HOL
now he's explaining why he trusts machine output more than anyone
Formal reasoning with the usual process of pen-and-paper mathematical proof neither scales as we would like in software verification nor has the expected degree of rigour.
you know humans made isabelle/HOL too right
-
now he's explaining why he trusts machine output more than anyone
Formal reasoning with the usual process of pen-and-paper mathematical proof neither scales as we would like in software verification nor has the expected degree of rigour.
you know humans made isabelle/HOL too right
"scales" i think he literally just means deskilling here. he's literally saying actually formal verification is more reliable than engineers you pay money to
-
"scales" i think he literally just means deskilling here. he's literally saying actually formal verification is more reliable than engineers you pay money to
now he's trying to mansplain "algorithmic verification" as if model checking in TLA+ https://lamport.azurewebsites.net/tla/high-level-view.html isn't actually extremely widely used in this exact space already
Research in this area has produced impressive results in recent years with improvements in the underlying theory and increased available computing power.
theory and computing power are the only things that produce impressive results. no i can't give you a citation it's not like this is my dissertation
They can catch increasingly wider classes of programmer errors
this is still a fucking hateful way to talk about formal verification
and even guarantee the absence of certain types of bugs.
such a half-assed phd thesis. do you even believe in what you're saying
-
now he's trying to mansplain "algorithmic verification" as if model checking in TLA+ https://lamport.azurewebsites.net/tla/high-level-view.html isn't actually extremely widely used in this exact space already
Research in this area has produced impressive results in recent years with improvements in the underlying theory and increased available computing power.
theory and computing power are the only things that produce impressive results. no i can't give you a citation it's not like this is my dissertation
They can catch increasingly wider classes of programmer errors
this is still a fucking hateful way to talk about formal verification
and even guarantee the absence of certain types of bugs.
such a half-assed phd thesis. do you even believe in what you're saying
@hipsterelectron TLA mentioned let's go -
@hipsterelectron TLA mentioned let's go
-
now he's trying to mansplain "algorithmic verification" as if model checking in TLA+ https://lamport.azurewebsites.net/tla/high-level-view.html isn't actually extremely widely used in this exact space already
Research in this area has produced impressive results in recent years with improvements in the underlying theory and increased available computing power.
theory and computing power are the only things that produce impressive results. no i can't give you a citation it's not like this is my dissertation
They can catch increasingly wider classes of programmer errors
this is still a fucking hateful way to talk about formal verification
and even guarantee the absence of certain types of bugs.
such a half-assed phd thesis. do you even believe in what you're saying
Proof creation has a high cost associated with it.
yeah you keep saying it sucks. aren't you supposed to fix things like that
To give an idea, it has been the author’s experience [93, 94, 96] that, in an interactive theorem prover, verifying the functional correctness of C code can require between one and two orders of magnitude more proof steps than line count,
(a) yeah maybe cause you keep trying to verify functional correctness guarantees about heap allocations in ring 0
(b) "line count" appeals to the VC class. it doesn't work on programmers
