Most who read that would expect the bug fixed in the linked GitHub PR to be impossible. The loophole was that the specification had a flaw, which was only mentioned as a vague hint about “unexpected features”.
You keep dancing around the question of it being a memory corruption despite confidently asserting it as a clear, indisputable fact. Please support your claim by identifying the specific memory safety property that was violated and how it was violated.
I provided citations. Use them and do your own research. I think you will find the answers in what the seL4 developers published, but I have no interest in spending days or even weeks pointing to things until you are satisfied.
You made a strong claim which you have failed to support adequately and yet have continued to double down on.
I did my research and presented my own interpretation which fundamentally disagrees with your interpretation. You have refused to address it, instead continuing to assert your interpretation without further detail. That does not prove my interpretation is correct, but it does indicate that the citations and evidence you have provided do not clearly lead to your conclusion and you neither identify the errors of my interpretation or directly demonstrate the correctness of your interpretation which could be done by demonstrating a simple counter-example demonstrating what memory is corrupted.
You claim it is indisputable fact, yet you claim it would take "days or even weeks" to present a clear example of the corruption. I do not see how you can claim the bug is clearly and indisputably a memory corruption bug that anybody can see from the citations you provided when it would take even you so long to provide a clear example.
I will say this. The seL4 developers made the strong claim. Evidence that it is not as strong as people who heard about it thought is not a strong claim. It is just being realistic. The seL4 developers themselves say that the properties they list are things that come out of the proof and your approach of looking for properties that they promise is a backward way of going about things, since they did not claim to exhaustively list all properties.
If you want to understand things to your satisfaction, read the proof and figure it out yourself. I have already understood things to my satisfaction and the double digit number of upvotes that I have received suggests to me that my explanation was to others’ satisfactions as well. You likely have many days or weeks or work ahead of you to answer a passing curiosity of yours whose precise answer is not going to change anything for anyone. Have fun.
https://docs.sel4.systems/projects/sel4/frequently-asked-que...
Most who read that would expect the bug fixed in the linked GitHub PR to be impossible. The loophole was that the specification had a flaw, which was only mentioned as a vague hint about “unexpected features”.