You're thinking like a language designer rather than a black-hat hacker :)
> All resources in a capability system are designated by capabilities, just like all objects in a memory safe language are designed by references.
The problem is that data doesn't begin life as a typed object but as a string of bits. I.e. it passes some "IO barrier" between the outside world and the world controlled by the language. At some point, some code must assign those bits to an object, and this code could be vulnerable.
> If a user has a capability to some resource, they are by definition authorized to access it.
This is defining whatever the program does as being correct, but that is not what we usually mean by correctness [1]. It's like saying that anyone who has obtained root privileges is, by definition, authorised to have them.
I fully understand the point about what is attainable and what isn't, but this is another example of my point about how some who think about correctness focus on what can be done without properly considering how much what can be done is worth, which is defined entirely but what needs to be done (or what's desired). The thing that I, the application's owner, want is not to have my data protected by a programming language's type system or, say, by means of a fuzzer but to have my data not leak to people I don't want to give my data to. In the case of security, the attacker would always go after the weakest point, whatever it is, and the question is by how much you've reduced the chances of a successful attack and at what cost.
Saying I can't give you what you want but here's what I can give you is perfectly fine, but how much what you can give me is worth to me depends entirely on how much it covers what I want. The value of reducing the chance of a successful attack by 70% is the same regardless of the means by which you achieve it, and then becomes purely a matter of cost.
I fully understand the difficulty of judging probabilities, but you need to understand that that is the sole source of value in correctness. But what I want is to lower the probability of some failure as much as possible for my $100 of investment. I don't care how it's done. That means that debates over assurance methods should be grounded in that question of cost and value. What makes an assurance method better or worse than another isn't how sound it is but how much it costs per unit of value, which is fault reduction (obviously the cost isn't linear). Soundness is a technique for the purpose of controlling value and costs, which may be more or less effective depending on circumstances. The point is that it's a means not an end.
I don't take issue with anything you say here, just your earlier comments about how expensive and non-compositional soundness necessarily is. I just described a programming language with built-in access control that only needs to be verified once for memory safety and absence of ambient authority, and then you can build any system with it and declare security policies, compose them, and have them enforced for no more cost than any other language. So why wouldn't you?
There is no cost-benefit here, it's just benefit. This is why I keep pushing back on how you characterise soundness, it just doesn't necessarily entail the kinds of costs and non-compositionality that you describe.
> how expensive and non-compositional soundness necessarily is
It is "deeper" properties (these are defined more robustly as those requiring a greater number of alternating universal and existential quantifiers) that are usually non-compositional and expensive to prove (and soundness means proof). Simple properties are easy to prove and can be made compositional, but they're also less valuable.
> So why wouldn't you?
No reason, except for the fact that you've defended against things that are easy to defend against easily and didn't defend against the hard things. In other words, of course you should prove as many properties as you can for a low cost, but don't exaggerate what it is that you've gained by doing so. That is precisely the delta between "can" and "need" that I was referring to. It's cool that I can get some extra security cheaply, but if that extra security amounts to 5%, then its value is not that high.
> There is no cost-benefit here, it's just benefit.
Of course there is. When the benefit is low then it's particularly easy to offset by other concerns, e.g. the speed at which I can churn out code or the cost of writing a compiler for an exotic architecture, a relatively common concern in the embedded space.
In any event, I always prefer typed languages when building big/important software (I've rarely used untyped languages), but remember that the original post is not about the simple properties that we get cheaply in typed languages, but how non-aliasing can make proving deeper properties easier. And what I was saying is that these proofs are nowhere near cost effective in most cases even after they've made a little easier.
> and have them enforced for no more cost than any other language
By which I mean that you get the sound policy enforcement for free, without any additional programming effort, where in typical programming languages this isn't the case.
> All resources in a capability system are designated by capabilities, just like all objects in a memory safe language are designed by references.
The problem is that data doesn't begin life as a typed object but as a string of bits. I.e. it passes some "IO barrier" between the outside world and the world controlled by the language. At some point, some code must assign those bits to an object, and this code could be vulnerable.
> If a user has a capability to some resource, they are by definition authorized to access it.
This is defining whatever the program does as being correct, but that is not what we usually mean by correctness [1]. It's like saying that anyone who has obtained root privileges is, by definition, authorised to have them.
I fully understand the point about what is attainable and what isn't, but this is another example of my point about how some who think about correctness focus on what can be done without properly considering how much what can be done is worth, which is defined entirely but what needs to be done (or what's desired). The thing that I, the application's owner, want is not to have my data protected by a programming language's type system or, say, by means of a fuzzer but to have my data not leak to people I don't want to give my data to. In the case of security, the attacker would always go after the weakest point, whatever it is, and the question is by how much you've reduced the chances of a successful attack and at what cost.
Saying I can't give you what you want but here's what I can give you is perfectly fine, but how much what you can give me is worth to me depends entirely on how much it covers what I want. The value of reducing the chance of a successful attack by 70% is the same regardless of the means by which you achieve it, and then becomes purely a matter of cost.
I fully understand the difficulty of judging probabilities, but you need to understand that that is the sole source of value in correctness. But what I want is to lower the probability of some failure as much as possible for my $100 of investment. I don't care how it's done. That means that debates over assurance methods should be grounded in that question of cost and value. What makes an assurance method better or worse than another isn't how sound it is but how much it costs per unit of value, which is fault reduction (obviously the cost isn't linear). Soundness is a technique for the purpose of controlling value and costs, which may be more or less effective depending on circumstances. The point is that it's a means not an end.