Biblio

Campus Companies and network operators perform risk assessment to inform policy-making, guide infrastructure investments or to comply with security standards such as ISO 27001. Due to the size and complexity of these networks, risk assessment techniques such as attack graphs or trees describe the attacker with a finite set of rules. This characterization of the attacker can easily miss attack vectors or overstate them, potentially leading to incorrect risk estimation. In this work, we propose the first methodology to justify a rule-based attacker model. Conceptually, we add another layer of abstraction on top of the symbolic model of cryptography, which reasons about protocols and abstracts cryptographic primitives. This new layer reasons about Internet-scale networks and abstracts protocols.We show, in general, how the soundness and completeness of a rule-based model can be ensured by verifying trace properties, linking soundness to safety properties and completeness to liveness properties. We then demonstrate the approach for a recently proposed threat model that quantifies the confidentiality of email communication on the Internet, including DNS, DNSSEC, and SMTP. Using off-the-shelf protocol verification tools, we discover two flaws in their threat model. After fixing them, we show that it provides symbolic soundness.

Security research has made extensive use of exhaustive Internet-wide scans over the recent years, as they can provide significant insights into the overall state of security of the Internet, and ZMap made scanning the entire IPv4 address space practical. However, the IPv4 address space is exhausted, and a switch to IPv6, the only accepted long-term solution, is inevitable. In turn, to better understand the security of devices connected to the Internet, including in particular Internet of Things devices, it is imperative to include IPv6 addresses in security evaluations and scans. Unfortunately, it is practically infeasible to iterate through the entire IPv6 address space, as it is 2ˆ96 times larger than the IPv4 address space. Therefore, enumeration of active hosts prior to scanning is necessary. Without it, we will be unable to investigate the overall security of Internet-connected devices in the future. In this paper, we introduce a novel technique to enumerate an active part of the IPv6 address space by walking DNSSEC-signed IPv6 reverse zones. Subsequently, by scanning the enumerated addresses, we uncover significant security problems: the exposure of sensitive data, and incorrectly controlled access to hosts, such as access to routing infrastructure via administrative interfaces, all of which were accessible via IPv6. Furthermore, from our analysis of the differences between accessing dual-stack hosts via IPv6 and IPv4, we hypothesize that the root cause is that machines automatically and by default take on globally routable IPv6 addresses. This is a practice that the affected system administrators appear unaware of, as the respective services are almost always properly protected from unauthorized access via IPv4. Our findings indicate (i) that enumerating active IPv6 hosts is practical without a preferential network position contrary to common belief, (ii) that the security of active IPv6 hosts is currently still lagging behind the security state of IPv4 hosts, and (iii) that unintended IPv6 connectivity is a major security issue for unaware system administrators.

The Domain Name System (DNS) is part of the core of the Internet. Over the past decade, much-needed security features were added to this protocol, with the introduction of the DNS Security Extensions. DNSSEC adds authenticity and integrity to the protocol using digital signatures, and turns the DNS into a public key infrastructure (PKI). At the top of this PKI is a single key, the so-called Key Signing Key (KSK) for the DNS root. The current Root KSK was introduced in 2010, and has not changed since. This year, the Root KSK will be replaced for the first time ever. This event potentially has a major impact on the Internet. Thousands of DNS resolvers worldwide rely on this key to validate DNSSEC signatures, and must start using the new key, either through an automated process, or manual intervention. Failure to pick up the new key will result in resolvers becoming completely unavailable to end users. This work presents the "Root Canary", a system to monitor and measure this event from the perspective of validating DNS resolvers for its entire nine-month duration. The system combines three active measurement platforms to have the broadest possible coverage of validating resolvers. Results will be presented in near real-time, to allow the global DNS community to act if problems arise. Furthermore, after the Root KSK rollover concludes in March 2018, we will use the recorded datasets for an in-depth analysis, from which the Internet community can draw lessons for future key rollovers.

Existing security mechanisms for managing the Internet infrastructural resources like IP addresses, AS numbers, BGP advertisements and DNS mappings rely on a Public Key Infrastructure (PKI) that can be potentially compromised by state actors and Advanced Persistent Threats (APTs). Ideally the Internet infrastructure needs a distributed and tamper-resistant resource management framework which cannot be subverted by any single entity. A secure, distributed ledger enables such a mechanism and the blockchain is the best known example of distributed ledgers. In this paper, we propose the use of a blockchain based mechanism to secure the Internet BGP and DNS infrastructure. While the blockchain has scaling issues to be overcome, the key advantages of such an approach include the elimination of any PKI-like root of trust, a verifiable and distributed transaction history log, multi-signature based authorizations for enhanced security, easy extensibility and scriptable programmability to secure new types of Internet resources and potential for a built in cryptocurrency. A tamper resistant DNS infrastructure also ensures that it is not possible for the application level PKI to spoof HTTPS traffic.

In this paper, we present a formal model for the verification of the DNSsec Protocol in the interactive theorem prover Isabelle/HOL. Relying on the inductive approach to security protocol verification, this formal analysis provides a more expressive representation than the widely accepted model checking analysis. Our mechanized model allows to represent the protocol, all its possible traces and the attacker and his knowledge. The fine grained model allows to show origin authentication, and replay attack prevention. Most prominently, we succeed in expressing Delegation Signatures and proving their authenticity formally.