Model Checking Projects for Security
Summary
Model checking, also known as finite-state analysis, involves using verification tools to exhaustively search all execution sequences for desired properties in a system or protocol specification, given some model of the powers of an attacker. While this process often reveals errors, the absence of errors does not imply correctness of the protocol. This method has been successfully applied in a number of academic papers: see here for further details.
Here is a repository of the security model-checking projects done by graduate and advanced undergraduate students in the Winter 2011 edition of CS259 at Stanford. The linked project archives contain a write-up of the study, a presentation, and relevant source code.
Projects using Murphi
OAuth 2.0 Implicit Grant Flow -- Quinn Slack and Roy Frostig
Summary:We used Murphi to analyze the security of OAuth 2.0 implicit grant flow, as specified in draft-ietf-oauth-v2-13. Our analysis uncovered an attack by which a Web attacker can cause a user’s account on an OAuth client to be associated with the attacker’s account on an OAuth authentication server. We propose a modification to the OAuth 2.0 protocol to prevent this attack.
Project Files
OpenID Attribute Exchange -- Ben Shapero and Srinivasan Iyer
Summary:The OpenID protocol is a single sign-on (SSO) protocol designed to allow users to use one single username and password across multiple websites. A key feature of the protocol is the ability to add extensions, increasing the capabilities of the protocol. One such extension is the Attribute Exchange extension. In the basic OpenID protocol, there is no ability for websites to define or use custom attributes beyond a small set of identifiers. For websites that need access to more than just an email address to function, the Attribute Extension protocol allows for a more detailed set of attributes to be exchanged. Currently, this extension is not widely implemented by relying parties (RPs), but three major OpenID providers (OPs), Google, Yahoo, and myopenid.com, support the extension. Our concern with this extension is the possibility that a RP can request more information from the OP about the user than the user wants/allows. Modeling the protocol formally is not enough to fully analyze the security of this protocol, as many of the extension’s details are either unspecified or left to the provider’s implementation. Instead, our project focuses on simulating a relying party that makes requests to the three OPs and observing the differing behaviors of all three.
Project Files
OpenID Phishing Analysis -- Sonal Mittal and Ben Phillips
Summary:Federated identity management tools aim to reduce redundant user credentialing activity on the Internet. The OpenID protocol falls under this branch of authentication mechanisms as it allows users to login to various websites using the credentials they have registered with an independent OpenID provider. Each provider is given significant range to implement the details of the protocol because the protocol itself is outlined in very broad strokes. For instance, details about the login process and “quick modes” are considered beyond the scope of the protocol specification. Such generality means that many observable security vulnerabilities fall outside the scope of the protocol. Most clearly, the protocol is vulnerable to a devastating phishing attack—it offers no recourse against a faked OpenID provider. Though the protocol does not purport to protect against phishing attacks, we believe that the growing prevalence of OpenID integration and usage warrants atten- tion to this security shortcoming. Using finite state analysis, we explore whether two user-side protocol extensions mitigate phishing vulnerabilities in OpenID.
Project Files
N-Ping protocol -- Ravi Kerur and David Fifield
Summary:Nping is a network diagnostic tool that can generate a variety of network packets and measure the responses that they provoke from a remote host. The classic example of this type of measurement is sending an ICMP Echo Request and receiving an ICMP Echo Reply or Destination Unreachable, but other possibilities include sending ARP requests to receive ARP replies, or sending TCP SYNs to receive, perhaps, SYN/ACK or RST. We present an analysis of NEP using the Murphi model checker. We show attacks against the protocol as it is deployed, as well as some against reduced versions of the protocol that demonstrate the need for certain protocol features or that might work if the protocol were incorrectly implemented.
Project Files
IPv6 Mobility -- Kushal Tayal, Kiran Isaac Abraham and Siddhi Soman
Summary:IpV6 is designed to solve the address space problems that exist with IPv4. The address space in IPv6 has been increased to 128 bits. This means that a lot more devices can be allocated with IP addresses. It is predicted that during the lifetime of IPv6 a majority of the devices will be mobile device. Hence, there is a need to provide support for mobility within IPv6. The support for mobility is still currently in the draft stages. The current RFC is 3775. RFC 3776 provides information on how IPSEC should be configured for use with IPv6. During the study, we used the Internet draft of RFC 3775 as reference. We find a number of attacks on the IPv6 Mobility, including Man-in-the-Middle, DDoS, and DoS. We also propose fixes for these attacks.
Project Files
Secure Cookie Protocol -- Jeremy Brotherton and Kiyoshi Shikuma
Summary:Much of HTTP cookie communications takes place in clear-text, allowing an attacker to gain sensitive information or perform other attacks. The use of additional transport layer security protocols such as SSL, in conjunction with the "secure" cookie attribute, can provide additional security properties. Alex Liu, et. al advocate here that a secure cookie protocol should provide authentication, confidentiality, integrity and anti-replay properties. This paper explores the four security properties proposed using techniques covered in CS259 at Stanford University. Through our analysis, we were able to identify several attacks against the protocol that will be detailed in this paper. In addition, we will explore a real-world example of this protocol as implemented by WordPress.
Project Files
TESLA -- Nina Chen and David Keeler
Summary:We used the finite state model checker Murphi to model TESLA, a broadcast authentication protocol. This protocol aims for efficiency, low overhead, scalability, and tolerance of packet loss. The success of the protocol largely depends on a model of senders and receivers, where the receivers are loosely time synchronized with the sender. Our model confirms most of the desired properties of the protocol, such as packet loss tolerance and minimal message buffering. We were also able to find an attack that exploits the time synchronization assumption, as well as some basic denial of service attacks.
Project Files
BitCoin -- Ruven Chu and Andrew He
Summary:We present our methodology for analyzing the security properties of the Bitcoin cryptocurrency. We use the formal verifier tool Murphi to investigate the double-spending problem, finding two known attacks using state enumeration. We briefly discuss the lack of true anonymity in Bitcoin transactions as well as Bitcoin's robustness against denial-of-service attacks.
Project Files
Location Privacy via private proximity testing -- Mugdha Lakhani
Summary:The system I studied presents three protocols for determining proximity of two nodes without compromising their location information. The authrors present the idea of "location tags" generated from the physical environment to strengthen the privacy guarantees of the protocols. Here I present the model of the first two of those protocols, and discuss possible attacks and fixes. Both the protocols are vulnerable to online dictionary attacks, identity spoofing and denial of service. I found that the use of location tags in necessary to provide the very basic privacy guarantees. I suggest some fixes that make the protocols immune to these attacks.
Project Files
Object-Capability Patterns -- Deian Stefan
Summary:Object Capability (OCap) patterns provide an alternative, more secure, approach to building systems following the principle of least authority. Despite the increasing popularity and application of OCap patterns, little effort has been put into the analysis of these patterns. We analyze several OCap patterns using the Murphi verification tool. Our results confirm previous vulnerabilities found in several OCap patterns when used in an operating systems context. We verify an attack on the sealer/unsealer pattern using the Joe-E with Java threads. Finally, we propose alternative patterns that our model checking did not find to be vulnerable. We including code that further demonstrates their usability.
Project Files
Real-time Protocols: SIP, Secured SIP, and SRTP -- Alexander Churchill and Emmanouel Liodakis
Summary:The Session Initiation Protocol (SIP) is a signaling protocol designed to control multime- dia communication sessions. The basic structure of SIP involves registration with a proxy server, calls to invite, ring, and ready, a media session, and bye messages with acknowl- edgements. Because SIP is designed for flexibility across devices and simplicity, there is no implicit security in the SIP protocol. The SIP standard described in RFC 3621 includes suggested security protocols designed to provide user-to-user security across the protocol. The Secure Real-time Transport Protocol (SRTP) is a profile of RTP designed to provide message security, authentication, integrity, and replay protection across media sessions. In this paper, we analyze the security of the standard implementation of SIP, the recommended secure implementation of SIP as per RFC 3621, and the security of a media session sent over SRTP.
Project Files
Projects using Alloy
Facebook Connect Analysis -- Abe Parvand and Steven Elia
Summary:Facebook provides an API for developers to leverage Facebook to authenticate users. Facebook also uses this API to allow third-party applications to interact with users in such a way that users can authorize applications and grant them certain permissions to access the users’ data. Using Alloy, we were able to verify all of the security properties under a web attacker model, and only one vulnerability under a more general network attacker model.
Project Files
Satellite Prefeching Proxy -- Brian Jones
Summary:This project, proposed by HughesNet, examines security vulnerabilities associated with using a prefetching proxy. Hughes is interested in using a prefetching proxy to reduce noticeable latency on the user's end while connected to the internet via satellite. This paper looks at three possible threats to this system, security properties associated with these threats, and possible solutions.
Project Files