No Arabic abstract
Off-chain protocols constitute one of the most promising approaches to solve the inherent scalability issue of blockchain technologies. The core idea is to let parties transact on-chain only once to establish a channel between them, leveraging later on the resulting channel paths to perform arbitrarily many peer-to-peer transactions off-chain. While significant progress has been made in terms of proof techniques for off-chain protocols, existing approaches do not capture the game-theoretic incentives at the core of their design, which led to overlooking significant attack vectors like the Wormhole attack in the past. This work introduces the first game-theoretic model that is expressive enough to reason about the security of off-chain protocols. We advocate the use of Extensive Form Games - EFGs and introduce two instances of EFGs to capture security properties of the closing and the routing of the Lightning Network. Specifically, we model the closing protocol, which relies on punishment mechanisms to disincentivize the uploading on-chain of old channel states, as well as the routing protocol, thereby formally characterizing the Wormhole attack, a vulnerability that undermines the fee-based incentive mechanism underlying the Lightning Network.
Large software platforms (e.g., mobile app stores, social media, email service providers) must ensure that files on their platform do not contain malicious code. Platform hosts use security tools to analyze those files for potential malware. However, given the expensive runtimes of tools coupled with the large number of exchanged files, platforms are not able to run all tools on every incoming file. Moreover, malicious parties look to find gaps in the coverage of the analysis tools, and exchange files containing malware that exploits these vulnerabilities. To address this problem, we present a novel approach that models the relationship between malicious parties and the security analyst as a leader-follower Stackelberg security game. To estimate the parameters of our model, we have combined the information from the VirusTotal dataset with the more detailed reports from the National Vulnerability Database. Compared to a set of natural baselines, we show that our model computes an optimal randomization over sets of available security analysis tools.
We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol, where timing information allows the study of different attack scenarios. We model check the protocols using UPPAAL. Further, a taxonomy is obtained by studying and categorising protocols from the well known Clark Jacob library and the Security Protocol Open Repository (SPORE) library. Finally, we present some new challenges and threats that arise when considering time in the analysis, by providing a novel protocol that uses time challenges and exposing a timing attack over an implementation of an existing security protocol.
The Nakamoto longest chain protocol is remarkably simple and has been proven to provide security against any adversary with less than 50% of the total hashing power. Proof-of-stake (PoS) protocols are an energy efficient alternative; however existing protocols adopting Nakamotos longest chain design achieve provable security only by allowing long-term predictability (which have serious security implications). In this paper, we prove that a natural longest chain PoS protocol with similar predictability as Nakamotos PoW protocol can achieve security against any adversary with less than 1/(1+e) fraction of the total stake. Moreover we propose a new family of longest chain PoS protocols that achieve security against a 50% adversary, while only requiring short-term predictability. Our proofs present a new approach to analyzing the formal security of blockchains, based on a notion of adversary-proof convergence.
Knowledge flow analysis offers a simple and flexible way to find flaws in security protocols. A protocol is described by a collection of rules constraining the propagation of knowledge amongst principals. Because this characterization corresponds closely to informal descriptions of protocols, it allows a succinct and natural formalization; because it abstracts away message ordering, and handles communications between principals and applications of cryptographic primitives uniformly, it is readily represented in a standard logic. A generic framework in the Alloy modelling language is presented, and instantiated for two standard protocols, and a new key management scheme.
Internet of Things (IoT) devices and applications can have significant vulnerabilities, which may be exploited by adversaries to cause considerable harm. An important approach for mitigating this threat is remote attestation, which enables the defender to remotely verify the integrity of devices and their software. There are a number of approaches for remote attestation, and each has its unique advantages and disadvantages in terms of detection accuracy and computational cost. Further, an attestation method may be applied in multiple ways, such as various levels of software coverage. Therefore, to minimize both security risks and computational overhead, defenders need to decide strategically which attestation methods to apply and how to apply them, depending on the characteristic of the devices and the potential losses. To answer these questions, we first develop a testbed for remote attestation of IoT devices, which enables us to measure the detection accuracy and performance overhead of various attestation methods. Our testbed integrates two example IoT applications, memory-checksum based attestation, and a variety of software vulnerabilities that allow adversaries to inject arbitrary code into running applications. Second, we model the problem of finding an optimal strategy for applying remote attestation as a Stackelberg security game between a defender and an adversary. We characterize the defenders optimal attestation strategy in a variety of special cases. Finally, building on experimental results from our testbed, we evaluate our model and show that optimal strategic attestation can lead to significantly lower losses than naive baseline strategies.