> that's a weird execution for any useful definition of "weird".
Weird execution is a term of art in the security biz. This is not that.
Weird execution happens when the attacker can control all of memory, not just objects the victim program rightly loaded from the heap.
> Your central claim is that you can take any old C program, compile it with Fil-C, and get a memory-safe C program.
Yes. Your program is memory safe. You get to access P1 if p pointed at P1.
You don’t get to define what memory safety means in Fil-C. I have defined it here: https://fil-c.org/gimso
Not every memory safe language defines it the same way. Python and JavaScript have a weaker definition since they both have powerful reflection including eval and similar superpowers. Rust has a weaker definition if you consider that you can use `unsafe`. Go has a weaker definition if you consider that tearing in Go leads to actual weird execution (attacker gets to pop the entire Go type system). Java’s definition is most similar to Fil-C’s, but even there you could argue both ways (Java has more unsafe code in its implementation while Fil-C doesn’t have the strict aliasing of Java’s type system).
You can always argue that someone else’s language isn’t memory safe if you allow yourself to define memory safety in a different way. That’s not a super useful line of argumentation, though it is amusing and fun
Sorry to intrude on the discussion, but I have a hard time grasping how to produce the behavior mentioned by quotemstr. From what I understand the following program would do it:
int arr1[] = {1, 2, 3, 4, 5};
int arr2[] = {10, 20, 30, 40, 50};
int *p1 = &arr1[1];
int *p2 = &arr2[2];
int *p = choose_between(p1,p2);
//then sometime later, a function gets passed p
// and this snippet runs
if (p == p2) {
//p gets torn by another thread
return p; // this allows an illegal index/pointer combo, possibly returning p1[1]
}
Is this program demonstrating the issue? Does this execute under Fil-C's rules without a memory fault? If not, could you provide some pseudocode that causes the described behavior?> Rust has a weaker definition if you consider that you can use `unsafe`
I don't see it. Rust makes the same guarantees regardless of the unsafe keyword. The difference is only that with the unsafe keyword you the programmer are responsible for upholding those guarantees whereas the compiler can check safe Rust.
You may define "memory safety" as you like. I will define "trustworthy system" as one in which the author acknowledges and owns limitations instead of iteratively refining private definitions until the limitations disappear. You can define a mathematical notation in which 2+3=9, but I'm under no obligation to accept it, and I'll take the attempt into consideration when evaluating the credibility of proofs in this strange notation.
Nobody is trying to hide the existence of "eval" or "unsafe". You're making a categorical claim of safety that's true only under a tendentious reading of common English words. Users reading your claims will come away with a mistaken faith in your system's guarantees.
Let us each invest according to our definitions.