CoFee: Teaching secure C Programming

CoFee is a modular framework focusing on code security and code robustness by using state-of-the-art software analyzers. Further, error messages are supplemented by meaningful hints suited for novice students. It also follows the theory of situated learning by exposing students to typical software engineering workflows using Gitlab for version control, continuous integration and code quality reports. To check code quality CoFee supports well-established open-source tools which were tested on a purpose build test suite. Its modular architecture allows easy integration of future analyzers.


Publications

Automated Detection of Bugs in Error Handling for Teaching Secure C Programming
Max Schrötter, Maximilian Falk and Bettina Schnor
Accepted for the sixth workshop: Automatische Bewertung von Programmieraufgaben (ABP 2023)
Munich, Germany, October 2023


Leveraging Continuous Feedback in Education to Increase C Code Quality
Max Schrötter and Bettina Schnor
9th International Conference on Computational Science and Computational Intelligence (CSCI)
Las Vegas, NV, USA, December 2022

DNSSEC und DANE

Transport Layer Security (TLS) ist das Standardverfahren zum Verschlüsseln des Datentransports. Über eine PKI können digitale Zertifikate ausgestellt, verteilt und geprüft werden. Die Authentizität der verwendeten Zertifikate ist jedoch nicht immer gewährleistet.


Derzeit sind über 200 verschiedene CAs verfügbar, jede dieser CA kann Zertifikate für jeden beliebigen Hostnamen ausstellen. Wenn eine dieser CAs nachlässig bei der Systemsicherheit oder der Prüfung des Antragsstellers ist, kann sich ein Angreifer ein "gültiges" Zertifikat für einen Host erstellen lassen.


Hier kommt DANE ins Spiel! DANE definiert einen TLSA-Record, der den Hash des öffentlichen Schlüssels einer Domain oder eines Dienstes enthält.


Vorteile von DANE

  • DANE ermöglicht die Validierung des öffentlichen Schlüssels und erhöht die Vertrauenswürdigkeit der TLS-Verbindung
  • DANE verhindert bei Verwendung von STARTTLS Downgrade-Angriffe
  • DANE macht CAA-Records im DNS überflüssig
  • DANE verringert die Angriffsfläche, da man sich vorinstallierte Root-Zertifikate der CAs spart
  • DANE kann außerdem von Domaininhabern dazu genutzt werden, eigene Zertifikate auszustellen, ohne auf eine bestehende Zertifizierungsstelle (CA) zurückgreifen zu müssen. DANE bietet somit eine vom Zertifikatsvertrauen unabhängige Überprüfung der Authentizität des Servers.

Um Manipulationen des TLSA-RR durch beispielsweise einem MitM-Angriff zu vermeiden, wird DNSSEC vorausgesetzt. Mittels Signaturen garantiert DNSSEC, dass DNS-Informationen zu einer Domain authentisch sind und während der Übertragung nicht gefälscht wurden.


DNSSEC

Das Domain Name System Security Extension (DNSSEC) erweitert das Domain Name System hinsichtlich der Transportsicherheit und dient als Grundlage weiterer Sicherheitsanwendungen. Konzipiert wurde DNSSEC zum einen, um eine Datenintegrität bezüglich der im DNS übertragenen Resource Records zu gewährleisten. Zum anderen soll eine Authentizität der Datenherkunft der übertragenen Resource Records sichergestellt sein.


DNS Hierarchie
Fig.1: DNS-Hierarchie in Form einer Baumstruktur

DNSSEC Chain of Trust

Figure 2 zeigt die Vertrauenskette für die autoritative Zone dnssec-uni-potsdam.de. Der autoritative Nameserver für dnssec-uni-potsdam.de enhält als letzte Instanz der Vertrauenskette in der Zonendatei einen Verweis auf mail.dnssec-uni-potsdam.de. Der öffentliche KSK-Teil liegt als Hash in dem DS-RR der übergeordneten Zone DE-NIC für die .de-Zone. Dieser signiert anschließend mit seinem KSK den DS-Eintrag. Nur der ZSK signiert die Zoneneinträge und stellt deren Integrität und Authentizität sicher. Der Schlüssel der übergeordneten Zonen (.de und root) signiert jeweils nur den DS-Eintrag im KSK. Bei einer Änderung des KSK ist eine out-of-band-Kommunikation mit der übergeordenten Zone nötig.

DNSSEC
Fig.2: DNSSEC Chain of Trust

Beispiel eines mit DANE abgesicherten Mailservers

Figure 3 zeigt den TLSA-Record für mail.dnssec-uni-potsdam.de. Der sendende Mailserver erhält aus dem DNS den MX- und den TLSA-Record des empfangenden Mailserver mail.dnssec-uni-potsdam.de. Mit dem TLSA-Record wird dem SMTP-Sender mitgeteilt, dass eine Kommunikation verschlüsselt erfolgen soll und nur einem Mailserver vertraut werden soll, der ein Zertifikat mit dem entsprechenden Fingerprint vorzeigt.

DANE
Fig.3: DANE-Architektur

Weblinks und Tools

DNSSEC und DANE in Praxis: [Slides] [Video]


Grundlagen DNSSEC
  • apnic - DNSSEC mit BIND
  • Doku LRZ - DNSSEC und DANE Dokumentation

Konfiguration DNSSEC

TOOLS

DANE RFCs

DNSSEC RFCs
  • RFC 4033 - Einführung in die DNS-Sicherheit/Anforderungen (2005)
  • RFC 4034 - Resource Records für DNS-Sicherheitserweiterung (2005)
  • RFC 4035 - Protokolländerungen für die DNS-Sicherheitserweiterungen (2005)
  • RFC 4470 - Minimale Abdeckung von NSEC-Datensätzen und DNSSEC-Onlinesignaturen (2006)
  • RFC 4641 - DNSSEC-Betriebsverfahren (2006)
  • RFC 5155 - DNS-Sicherheit (DNSSEC) Hashed Authenticated Denial of Existence (2008)
  • RFC 6014 - Zuweisung von Kennungen für kryptografische Algorithmen für DNSSEC (2010)
  • RFC 4641 - DNSSEC-Betriebsverfahren (2006)
  • RFC 6781 - DNSSEC-Betriebsverfahren Version 2 (2012)
  • RFC 7583 - Überlegungen zum DNSSEC-Schlüssel-Rollover-Timing (2015)

Literatur

Absicherung von Firmware-Updates im Internet der Dinge mittels DNSSEC/DANE
Miyana Sophie Stange, Masterarbeit
2022


Under the Hood of DANE Mismanagement in SMTP
Hyeonmin Lee, Ishtiaq Ashiq, Moritz Müller, Roland van Rijswijk-Deij, Taekyoung Kwon, Taejoong Chung
2022


Roll, Roll, Roll your Root: A Comprehensive Analysis of the First Ever DNSSEC Root KSK Rollover
M. Müller, W. Hardaker, M. Thomas, T. Chung, R. van Rijswijk-Deij, D. Wessels, W.
2019


The Impact of DNSSEC on the Internet Landscape
Matthäus Wander, Dissertation
Universität Duisburg-Essen
2015


Sicherheit im Domain Name System
Claas Lorenz, Bachelorarbeit
Universität Potsdam
2012


Publications

Securing SUIT-conform Firmware Update Management in the IoT with DNSSEC/DANE
Max Schrötter, Miyana Sophie Stange and Bettina Schnor
19th GI/ITG KuVS Fachgespräch: Drahtlose Sensornetze
Berlin, Germany, September 2022


Absicherung von Firmware-Updates im Internet der Dinge mittels DNSSEC/DANE
Miyana Sophie Stange, Masterarbeit

Fast Formal Verification of Network Security Compliance

“Security’s worst enemy is complexity.” Ferguson and Schneier


Originally, this famous quote targeted the standardization of the IPsec protocol suite but also bears some universal insight: the more complex a technical system becomes, the harder it gets to ensure its secure functioning as has been confirmed in practice several times. Throughout the recent years, IT landscapes have grown even more complex. Trends like Mobile Computing, Cloud Computing, or the Internet of Things introduced new opportunities for many if not most organizations and their adoption ultimatively increased the complexity of these organizations’ IT landscapes.

Our research aims at the practical reduction of complexity for security officials and administrators to effectively and efficiently handle security on the organizational as well as on the technical level. Particularly, we offer formal tooling to assess the state of network security compliance that can be used in standard workflows in information security management (ISM), e.g., BSI-Grundschutz or ISO 27001.


Approach

Approach on the evolution of a network towards network security compliance
Fig. 1: Approach on the evolution of a network towards network security compliance

Figure 1 depicts the general approach on how security officials and administrators can evolve the network towards security compliance and maintain the secure state once reached. It is required to:

  1. first, determine the status quo of network security,
  2. then, migrate towards the desired state as required by the ISM, and
  3. finally, maintain the desired state.

(Note: PDCA stands for Plan-Do-Check-Act and is a well-established standard approach in information security management, e.g., in ISO 27001.)

Workflow for the verification of network security compliance
Fig. 2: Workflow for the verification of network security compliance

As seen in Figure 2, the compliance verification workflow consists of three major parts – the specification of the security policy, the network modeling, and the compliance verification. At first, the security official needs to specify the security policy (1a). In this specification, access control is defined through reachabilities between organizational entities, e.g., services or network segments, that have been described in an inventory (1b) which is provided by the network administrator. The inventory maps the organizational terms, e.g., the organization’s ERP service or the research department’s network segment, to their technical implementation, e.g., a segment’s IP address range or a service’s protocol and port. Also, the network administrator provides the network’s configurations, e.g., firewall rule sets or routing configuration, that are to be modeled (1c). Then, the network model is verified for conformance with the security specification (2) and, finally, the result is reported (3) for further utilization by the security official and the network administrator.


Contributions

To enable security officials as well as network security administrators to practically determine the state of network security compliance and to overcome the performance limitations of general model checking approaches, we make the following major contributions:

  • Specification: We empower security officials and administrators to specify security policies in terms of an abstract language – namely the FaVe Policy Language (FPL). The FPL is highly usable as it operates on a level of abstraction suitable also for non-academically skilled personnel, e.g., many network administrators. FPL provides capabilities to concisely specify organizational structures in a hierarchical model using roles, groups of roles, and services. This way these entities are abstracted from their technical implementation, e.g., with VLANs, IP addresses, or ports. Policies are specified using these abstract terms which makes them concise and easily auditable for organizational compliance.
  • Modeling and Verification: In order to offer administrators an accessible and comprehensive way to model their networks, we introduce DHSA – a human-readable yet efficient formalism based on the notion of Header Spaces. We prototypically implemented DHSA in FaVe – our fast verification framework – which ships with a variety of predefined model templates for network devices and configurations including firewalls, routers, and switches. This way, modeling becomes an easy venture and further knowledge of DHSA is only needed when introducing new or altering existing device templates. Our implementation provides an efficient mapping of DHSA’s data structures onto classical HSA bitvector structures to benefit from the latter’s solving performance.
    In addition, we published FaVe as open source: https://github.com/cllorenz/fave-project.
  • Statefulness: FaVe’s fast compliance verification of FPL policies includes support for stateful packet filters. Statefulness poses a common verification challenge as it raises computational complexity. We present State Shell Interweaving – a modeling technique which efficiently projects stateful behaviour in DHSA models onto stateless capabilities. This allows networks that include stateful devices to be analysed efficiently. We evaluate our approach’s effectiveness and performance using a variety of well known as well as custom benchmarks.
  • Anomaly Detection: To enable the detection of firewall anomalies, we implemented a fast and scalable approach based on DHSA in FaVe. We show its effectiveness and scalability with well known as well as custom benchmarks with rule sets consisting of up to 15,000 rules.
  • Dynamic Protocols: In order to support state-of-the-art networking, we offer and evaluate IPv6 support including extension header chains. Their dynamic nature challenge the applicability of existing high speed verification approaches that operate on fixed size data models like HSA. The ability to dynamically extend the model at runtime is the key to successfully verify advanced security properties for complex IPv6 networks. We remain fully compatible with the still widely used IPv4.

These contributions enable security officials and administrators to gain and manage compliant network security.

This research is performed in close cooperation with the genua GmbH.


Publications

Firewall Management: Rapid Anomaly Detection
Claas Lorenz and Bettina Schnor
IEEE 24th International Conference on High Performance Computing (HPCC)
In this work, we leverage our domain oriented notion of the Header Space Analysis to detect firewall anomalies at previously unknown pace. Our approach outperforms approaches from literature by a factor of nearly 115 and analyzes a large real-world firewall rule set in well below a second.
Chengdu, China, December 2022


Continuous Verification of Network Security Compliance
Claas Lorenz and Vera Clemens and Max Schrötter and Bettina Schnor
IEEE Transactions on Network and Service Management (TNSM)
In this work, we present the concept of state shell interweaving to transform a stateful firewall rule set into a stateless rule set. This allows us to reuse any fast domain specific engine from the field of data plane verification tools leveraging smart, very fast, and domain specialized data structures and algorithms including Header Space Analysis (HSA).
June 2022


Modeling IPv6 Firewalls for Fast Formal Verification
Claas Lorenz, Sebastian Kiekheben and Bettina Schnor
International Conference on Networked Systems (NetSys)
Göttingen, Germany, March 2017


Anomaly Detection for Distributed IPv6 Firewalls
Claas Lorenz and Bettina Schnor
12th International Conference on Security and Cryptography (SECRYPT)
Colmar, France, July 2015

IPv6 Intrusion Detection System

The transition from the currently used internet protocol version IPv4 to the official successor protocol IPv6 is an important technical requirement for the ongoing development of communication and network infrastructures within the next years. Therefore the security of IPv6 networks is of high social relevance and importance.


The project "IPv6 Intrusion Detection System" is realized in collaboration of "University of Potsdam", "Beuth-Hochschule für Technik", "EANTC" and "Strato AG". It is supported by the German "Federal Ministry of Education and Research".


For further information please visit the project website: www.ipv6-ids.de