Protocols appear in many different forms in secure systems. They are used for secure authentication or communication (for example, the TLS protocol), for achieving resilience and scale in a distributed environment (for example, blockchain and cloud protocols), to enforcing secure uses of cryptographic libraries (for example, in API usage protocols). A system’s components may be individually secure, but a poorly designed or implemented protocol can nonetheless result in security failures. A typical protocol may be highly complex, involving the interaction between many different modules. As a result, errors in protocols are unfortunately common at both the design and implementation levels. Errors related to protocols can introduce the following problems:
- Data compromises. Protocols are often responsible for ensuring that data is securely communicated and stored, and protocol problems can result in exfiltration of data. This is a particular problem for network protocols because such systems are inherently open to attack on the public internet.
- Denial of service attacks. Protocols are used to ensure services remain highly available. Faulty protocols may result in attackers being able to shut down the service. The consequences of such attacks may be cost or customer dissatisfaction in the case of commercial web services or serious safety problems, such as time-sensitive cyber-physical systems.
- Authentication problems. Many protocols are used to authenticate users; that is, determine whether they can legitimately access a system. Mis-authentication can enable an attacker to launch further attacks through their stolen credentials.
- Data inconsistency or loss. Protocols are used in cloud services to ensure they are resilient against failures. Faulty protocols may result in loss or inconsistency of data, in the worst case allowing attackers to deceptively alter critical data.
Improper protocol design and implementations can manifest in several different ways:
- Insecure protocol design. Unlike core cryptography such as AES, which is generally secure in its design, it is common for protocols to harbour errors that subvert the protocol’s security goals. These range from basic errors to sophisticated attacks based on cryptanalysis of the protocol properties. TLS has been subject to many such attacks on its design during its lifespan.
- Improper protocol implementations. Protocols are often difficult to implement correctly in actual software. This is a result of the complexity of the protocols themselves and the fact that code is often spread across multiple modules and teams. The effects of this may be that the protocol can be made insecure, for example, by forcing it to transition into a low-security mode. An example of this is the Logjam attack against implementations of TLS.
- Protocol usage errors. Cryptographic and many other secure APIs often depend on users to adhere to usage protocols. An example is the rule that cryptographic nonces should be generated as distinct values before use. Well-designed APIs minimize the cases in which this can happen, but nonetheless, it is common for users to misuse protocols, and therefore undermine the security guarantees provided by cryptography.
Are you wondering if your protocol designs are free of errors? Do you want your protocol implementations or user code checked or audited? Galois can help with this and more. The following are examples of the services we can provide:
- Protocol design assurance. Galois can help during developing a new protocol or prototyping modifications to existing protocols. During this process, we typically develop formal models and systematic tests of the protocol design which are intended to catch protocol bugs early, before they reach production. These formal models can then be used as the foundation for more assurance work.
- Verification of protocol code. Galois can formally verify the implementation of protocols to ensure that they conform to the intended protocol behavior. To do this, we typically apply our verification tool suite SAW to your code, which results in a precise mathematical model of the code behavior. We can then use this model to compare with the intended protocol behavior, ultimately allowing us to eliminate mis-implemented protocol steps.
- Systematic protocol testing. Galois can systematically test implementations of protocols. Our approach involves building an executable model of the code and using this as a source of protocol inputs. Using this model, we can systematically explore all possible behaviors of the protocol. This is a black-box assurance approach, and can therefore be applied to complex systems where auditing code is infeasible.