Mohammed Almukaynizi, Vivin Paliath, Malay Shah, Malav Shah · 5 authors
With the recent prevalence of darkweb/deepweb (D2web) sites specializing in the trade of exploit kits and malware, malicious actors have easy-access to a wide-range of tools that can empower their offensive capability. In this study, we apply concepts from causal reasoning, itemset mining, and logic programming on historical cryptocurrency-related cyber incidents with intelligence collected from over 400 D2web hacker forums. Our goal was to find indicators of cyber threats targeting cryptocurrency traders and exchange platforms from hacker activity. Our approach found interesting activities that, when observed together in the D2web, subsequent cryptocurrency-related incidents are at least twice as likely to occur than they would if no activity was observed. We also present an algorithmic extension to a previously-introduced algorithm called APT-Extract that allows to model new semantic structures that are specific to our application.
Zaynah Dargaye, Antonella Del Pozzo, Sara Tucci-Piergiovanni
The paper presents Pluralize a formal logical framework able to extend the execution of blockchain transactions to events coming from external oracles, like external time, sensor data, human-made declarations, etc. These events are by essence non-reliable, since transaction execution can be triggered by information whose veracity cannot be established by the blockchain. To overcome this problem, the language features a first-order logic and an authority algebra to allow formal reasoning and establish accountability of agents for blockchain-enabled transactions. We provide an accountability model that allows to formally prove the accountability of agents by a formal proof locally executable by each agent of the blockchain.
At the heart of the Bitcoin is a blockchain protocol, a protocol for achieving consensus on a public ledger that records bitcoin transactions. To the extent that a blockchain protocol is used for applications such as contract signing and making certain transactions (such as house sales) public, we need to understand what guarantees the protocol gives us in terms of agents' knowledge. Here, we provide a complete characterization of agent's knowledge when running a blockchain protocol using a variant of common knowledge that takes into account the fact that agents can enter and leave the system, it is not known which agents are in fact following the protocol (some agents may want to deviate if they can gain by doing so), and the fact that the guarantees provided by blockchain protocols are probabilistic. We then consider some scenarios involving contracts and show that this level of knowledge suffices for some scenarios, but not others.
Abstract Blockchains are distributed data structures that are used to achieve consensus in systems for cryptocurrencies (like Bitcoin) or smart contracts (like Ethereum). Although blockchains gained a lot of popularity recently, there are only few logic-based models for blockchains available. We introduce $\mathsf{BCL}$, a dynamic logic to reason about blockchain updates, and show that $\mathsf{BCL}$ is sound and complete with respect to a simple blockchain model.
Kaylash Chaudhary, Ansgar Fehnker, Jaco van de Pol, Mariëlle Stoelinga
Bitcoin is a popular digital currency for online payments, realized as a decentralized peer-to-peer electronic cash system. Bitcoin keeps a ledger of all transactions; the majority of the participants decides on the correct ledger. Since there is no trusted third party to guard against double spending, and inspired by its popularity, we would like to investigate the correctness of the Bitcoin protocol. Double spending is an important threat to electronic payment systems. Double spending would happen if one user could force a majority to believe that a ledger without his previous payment is the correct one. We are interested in the probability of success of such a double spending attack, which is linked to the computational power of the attacker. This paper examines the Bitcoin protocol and provides its formalization as an UPPAAL model. The model will be used to show how double spending can be done if the parties in the Bitcoin protocol behave maliciously, and with what probability double spending occurs.