28 ms·

> And this has been a particular challenge for poor C++. If we prove a property then the property holds, but if we just found and meticulously fixed 846 of the

• naasking 2y ago
  > particularly if they're as complex as "an unauthorised user cannot obtain some information". Even a complete and total elimination of all memory safety bugs and all concurrency bugs won't get you anywhere near that goal Actually that's not really true. If you take that as a base and remove ambient authority, then you have capability security which does get you as close to fulfilling that property as is possible to achieve. I'd say that's pretty near that goal.
  • pron 2y ago
    I disagree, for multiple reasons: 1. You need to verify that all the sensitive data is indeed guarded with the appropriate capabilities. 2. You need to verify that the capability objects are created only after proper authorisation. 3. You need to verify that the capability objects cannot escape their relevant context. 4. You need to verify that the data is not accessible by "extra-program" means, e.g. the file containing the data may be read via a dumb directory-injection attack. Some simple sound techniques by the programming language can help with 3 and a part of 2, but not the rest. Indeed the current #1 top vulnerability [1] is a misconfigured or incorrect access control. [1]: https://owasp.org/www-project-top-ten/ https://owasp.org/www-project-top-ten/
    • naasking 2y ago
      Some background: 1. "An unauthorised user cannot obtain some information" is not a property that can be achieved by any access control system, even in theory, eg. an authorized user can just provide a copy to an unauthorized user. I will outline the only achievable property below. 2. All resources in a capability system are designated by capabilities, just like all objects in a memory safe language are designed by references. 3. You can obtain more capabilities by accessing capabilities contained within resources designated by other capabilities, just like you can obtain more references by accessing fields of objects that contain references. 4. Capabilities intrinsically combine designation with authorization. If a user has a capability to some resource, they are by definition authorized to access it. There is no such thing as a "context" in which a resource may or may not be accessed, you only either have or do not have a capability to it. 5. Capabilities are not ambient in the environment, and so the only path to obtaining capabilities is through the capability set you're given. An example of an ambient authority is the ability to obtain a file handle to any file in a system using an arbitrary file string you can just construct. Another example is being able to convert an arbitrary number into a reference, ie. violating memory safety. Hopefully it's now clear how there's a formal correspondence between capabilities and memory safe languages that have had ambient authority removed. This does not in any meaningful way restrict our ability to construct programs, at worst we must pass around a few more parameters that we used to access using ambient authorities (like File.Open). Access to resources can now only flow along the reference graph and security analysis now becomes tractable, basically another type of dataflow analysis. So the security property that you want to verify is that there is no way for user X to access resource Y if given capability set C. This means that the transitive closure of C doesn't include Y. There are numerous ways to achieve this, but the most trivial way is to use a typed language and create a type specifically to hold Y, and two capability set types for authorized and unauthorized users, and then you can ensure by simple inspection that a Y never appears in any reference placed in a C (or you can go more precise and only ensure that Y never appears in any return/escape position, thus allowing X to operate on Y's indirectly via some API). The type system is already a dataflow analysis, so this just piggybacks off of that to achieve the property you're after. Note that these are comparatively simple steps compared to getting memory safety to begin with. That said, I agree that "extra-program" means of undermining the foundation of one's secure system obviously undermines the security properties. This is not really a compelling objection to me anymore than the proof of the validity of an algorithm must assume that your computer correctly adds two numbers.