Analysing gossip mechanisms with PRISM
by Michael Oxford
Billions of internet connections rely on the use of public cryptographic keys to encrypt data. While this is necessary for safe browsing it is certainly not sufficient. In particular, how can I be confident that the public key I am using for a website does belong to the company I want to share my sensitive details with? If I exchange any bank details or passwords, I do not want them to go to an imposter as part of a phishing attack.
To validate the identity of websites, an independent third party called the certificate authority (CA) electronically signs a special document called a public key certificate and gives this to the owner of the website, allowing them to prove who they say they are. Anyone with access to a web browser can view these certificates by clicking on the green padlock next to the web address, showing the owner of the certificate, the issuer and how long the document is valid for (try it yourself on this page!).
Unfortunately, the conduct of CAs has been questioned during the past few years as their mishandling of certificates have led to serious disruptions of online services. A famous example is the defunct Dutch CA DigiNotar, where in 2011 it was revealed that at least 500 fraudulent certificates were issued in their name and no record was kept for them. Most of these certificates were used by many Dutch websites for financial transactions, leaving them vulnerable to outside interception by hackers.
Certificate transparency
Certificate Transparency (CT) is a new system developed by Google designed to make certificate distribution more accountable by instructing participating CAs to add newly signed certificates to a public, append-only log where its content cannot be modified or removed by anybody. To check if a certificate is present in the log or if a snapshot of the log is an extension of an older one, we can request a proof for either case which can be quickly found due to how items in the log are appended. While CT is not a complete solution to the problem of phishing attacks, this kind of public auditing is advantageous for companies if they want to search for any fake certificates issued in their name. At the time of writing, CT is used by Google Chrome and Mozilla Firefox plans to support it in the future.
CT is not without some faults. A powerful attacker with access to many resources, such as an authoritarian government, can control the internet connections of many users and redirect them all to a fake log which was created from an already existing one. This log, controlled and modifiable by the attacker, will contain thousands of fraudulent certificates that can be used to monitor the online activity of the targeted users and, because they are being made to contact the fake log, they will be duped into thinking that these certificates are genuine. Without a way for the users to check that they are accessing the same log as everybody else on Earth, they will never know that they are victims of a large-scale attack. We call such an attack a split-world attack. These large-scale attacks require large-scale solutions.
Gossiping
Simply put, gossiping is a technique where computers randomly share what they know about something through the internet to hundreds of other devices. It has been suggested for a long time that gossiping will help mitigate split-world attacks because if targeted victims are able to spread their log data (sourced from the fake log) to other users who are not affected from an attack, somebody will eventually find an inconsistency with the data they already have (sourced from the genuine log) and report this to everyone on the internet.
Gossip protocol designs have been proposed from Chuat et al and Nordberg et al but a common feature they all share is that users gossip with servers using messages that piggyback on secure connections (HTTPS). The data that is gossiped contains signed tree heads (STH), briefly describing the state the log was in when it generated it.
For our investigations we have chosen to focus on the Chuat et al protocol which comes in two varieties; one makes users gossip only one STH at a time and the other makes them gossip a pair of STHs with a proof. In these protocols, when STHs are being shared between two gossiping parties, they are checked on both sides to see if they are consistent with other STHs that they know about, contacting the log for a proof depending on certain circumstances. Afterwards, both parties update their memory cache with the retrieved data if it is newer than what they already have, deleting older STHs if necessary. An issue we have found is that not enough analysis has been done concerning how quick these protocols are in detecting split-world attacks and spreading data throughout a large network.
PRISM
Birmingham is one of the lead developers of the probabilistic model checking software PRISM, specialising in the analysis of computer systems that exhibit random behaviour. The software supports a variety of probabilistic models and temporal logics which we need as part of our investigation into analysing the gossip protocols from a security and efficiency perspective.
Our models attempt to closely replicate how the protocols and users behave in practice, with users randomly choosing a web-hosting server to gossip with. Using state-of-the-art algorithms, PRISM allows us to perform model checking techniques to quantitatively measure the probability of detection of a split-world attack and the number of times users need to contact the log when performing consistency checks. We also extended our models to make servers gossip with each other to see if the performance of the protocols can be further improved.
Findings
Our results indicate that the version of the protocol which gossips a pair of STHs with a proof is the most efficient protocol, requiring fewer log connections to execute. We can replicate this fact when we model this protocol in networks with lots of users. However, there is very little difference between both versions of the Chuat et al protocol in terms of detecting attacks; this is expected as the updating procedure is nearly identical.
Furthermore, by having servers randomly gossip with each other, we found that this additional communication significantly improves both security and connection overhead. We believe that incorporating this into the already existing protocols will help data to spread quickly to different clusters of users who congregate around certain web domains and unlikely to access various areas of the internet.
Without the tools that PRISM provides, these results would not have been possible to find but there is still so much to explore. For instance, can the protocols we have looked at so far be exploited in cyber-attacks other than split-world to make them even more dangerous? If such vulnerabilities exist, how can PRISM help us to patch them? Here at Birmingham, we hope to answer these questions and more.
The graphs show some of the results that we produced when investigating a simple split-world scenario where one client in a network of ten nodes was targeted. By measuring the amount of log connections made (the first graph), it appears that by using the protocol which gossips both STHs and proofs is the most efficient one. Additionally, having servers talk to each other provides great benefits to security (the second graph).
Find out more
Certificate transparency
- Ben Laurie. Certificate transparency. Queue, 12(8):10, 2014.
- CT website: https://www.certificate-transparency.org/
- Laurie, B., Langley, A., Kasper, E., Messerie, E. and Stradling, R., 2017. Certificate transparency version 2.0. RFC-bis 6962-bis.
Gossip protocols
- Chuat, L., Szalachowski, P., Perrig, A., Laurie, B. and Messeri, E., 2015, September. Efficient gossip protocols for verifying the consistency of certificate logs. In Communications and Network Security (CNS), 2015 IEEE Conference on (pp. 415-423). IEEE.
- Linus Nordberg, Daniel Kahn Gillmor, and Tom Ritter. Gossiping in CT. Internet-Draft draft-ietf-trans-gossip-05, Internet Engineering Task Force, 2018. Work in Progress.
PRISM model checker
- Kwiatkowska, M., Norman, G. and Parker, D., 2011, July. PRISM 4.0: Verification of probabilistic real-time systems. In International conference on computer aided verification (pp. 585-591). Springer, Berlin, Heidelberg.
- PRISM website: http://prismmodelchecker.org/