Search

A recent breakthrough in computer-assisted mathematics showed that every set of $30$ points in the plane in general position (i.e., without three on a common line) contains an empty convex hexagon, thus closing a line of research dating back to the 1930s. Through a combination of geometric insights and automated reasoning techniques, Heule and Scheucher constructed a CNF formula $\phi_n$, with $O(n^4)$ clauses, whose unsatisfiability implies that no set of $n$ points in general position can avoid an empty convex hexagon. An unsatisfiability proof for n = 30 was then found with a SAT solver using 17300 CPU hours of parallel computation, thus implying that the empty hexagon number h(6) is equal to 30. In this paper, we formalize and verify this result in the Lean theorem prover. Our formalization covers discrete computational geometry ideas and SAT encoding techniques that have been successfully applied to similar Erd\H{o}s-Szekeres-type problems. In particular, our framework provides tools to connect standard mathematical objects to propositional assignments, which represents a key step towards the formal verification of other SAT-based mathematical results. Overall, we hope that this work sets a new standard for verification when extensive computation is used for discrete geometry problems, and that it increases the trust the mathematical community has in computer-assisted proofs in this area., Comment: submitted to ITP 2024

In this paper, we revisit the use of honeypots for detecting reflective amplification attacks. These measurement tools require careful design of both data collection and data analysis including cautious threshold inference. We survey common amplification honeypot platforms as well as the underlying methods to infer attack detection thresholds and to extract knowledge from the data. By systematically exploring the threshold space, we find most honeypot platforms produce comparable results despite their different configurations. Moreover, by applying data from a large-scale honeypot deployment, network telescopes, and a real-world baseline obtained from a leading DDoS mitigation provider, we question the fundamental assumption of honeypot research that convergence of observations can imply their completeness. Conclusively we derive guidance on precise, reproducible honeypot research, and present open challenges., Comment: camera-ready

In this paper, we revisit the performance of the QUIC connection setup and relate the design choices for fast and secure connections to common Web deployments. We analyze over 1M Web domains with 272k QUIC-enabled services and find two worrying results. First, current practices of creating, providing, and fetching Web certificates undermine reduced round trip times during the connection setup since sizes of 35% of server certificates exceed the amplification limit. Second, non-standard server implementations lead to larger amplification factors than QUIC permits, which increase even further in IP spoofing scenarios. We present guidance for all involved stakeholders to improve the situation., Comment: camera-ready

In this paper, we study the potentials of passive measurements to gain advanced knowledge about QUIC deployments. By analyzing one month backscatter traffic of the /9 CAIDA network telescope, we are able to make the following observations. First, we can identify different off-net deployments of hypergiants, using packet features such as QUIC source connection IDs (SCID), packet coalescence, and packet lengths. Second, Facebook and Google configure significantly different retransmission timeouts and maximum number of retransmissions. Third, SCIDs allow further insights into load balancer deployments such as number of servers per load balancer. We bolster our results by active measurements., Comment: preprint

Context: Definition of Done (DoD) is one of the fundamental concepts of Scrum. It expresses a shared view of a Scrum Team on what makes an increment of their product complete. DoDs are often defined as checklists with items being requirements towards software (e.g., quality requirements) or towards activities performed to make the increment shippable (e.g., code reviews, testing). Unfortunately, the knowledge about the usefulness of DoD is still very limited. Objective: The goal is to study what benefits using the DoD practice can bring to an agile project, what problems it may trigger, and how it is created and maintained. Method: In the survey among members of agile software development projects, 137 practitioners from all over the globe shared their experience with us. Results: 93% of the respondents perceive DoD as at least valuable for their ventures. It helps them to make work items complete, assure product quality, and ensure the needed activities are executed. However, they indicated that every second project struggles with infeasible, incorrect, unavailable, or creeping DoD. Conclusions: It follows from the study that DoD is important but not easy to use and more empirical studies are needed to identify best practices in this area.

In this paper, we present the design, implementation, and analysis of DNS over CoAP (DoC), a new proposal for secure and privacy-friendly name resolution of constrained IoT devices. We implement different design choices of DoC in RIOT, an open-source operating system for the IoT, evaluate performance measures in a testbed, compare with DNS over UDP and DNS over DTLS, and validate our protocol design based on empirical DNS IoT data. Our findings indicate that plain DoC is on par with common DNS solutions for the constrained IoT but significantly outperforms when additional standard features of CoAP are used such as caching. With OSCORE, we can save more than 10 kBytes of code memory compared to DTLS, when a CoAP application is already present, and retain the end-to-end trust chain with intermediate proxies, while leveraging features such as group communication or encrypted en-route caching. We also discuss a compression scheme for very restricted links that reduces data by up to 70%., Comment: 25 pages, 15 figures, 6 tables; presented at CoNEXT 2023

The critical remote-code-execution (RCE) Log4Shell is a severe vulnerability that was disclosed to the public on December 10, 2021. It exploits a bug in the wide-spread Log4j library. Any service that uses the library and exposes an interface to the Internet is potentially vulnerable. In this paper, we measure the rush of scanners during the two months after the disclosure. We use several vantage points to observe both researchers and attackers. For this purpose, we collect and analyze payloads sent by benign and malicious communication parties, their origins, and churn. We find that the initial rush of scanners quickly ebbed. Especially non-malicious scanners were only interested in the days after the disclosure. In contrast, malicious scanners continue targeting the vulnerability., Comment: Proc. of Network Traffic Measurement and Analysis Conference (TMA '22), camera ready

Synapses play a critical role in memory, learning, and cognition. Their main functions include converting pre-synaptic voltage spikes to post-synaptic currents, as well as scaling the input signal. Several brain-inspired architectures have been proposed to emulate the behavior of biological synapses. While these are useful to explore the properties of nervous systems, the challenge of making biocompatible and flexible circuits with biologically plausible time constants and tunable gain remains. Here, a physically flexible organic log-domain integrator synaptic circuit is shown to address this challenge. In particular, the circuit is fabricated using organic-based materials that are electrically active, offer flexibility and biocompatibility, as well as time constants (critical in learning neural codes and encoding spatiotemporal patterns) that are biologically plausible. Using a 10 nF synaptic capacitor, the time constant reached 126 ms and 221 ms before and during bending, respectively. The flexible synaptic circuit is characterized before and during bending, followed by studies on the effects of weighting voltage, synaptic capacitance, and disparity in pre-synaptic signals on the time constant., Comment: Accepted by Advanced Electronic Materials (18 pages, 17 figures)

In 1982, Raymond Smullyan published an article, "The Asylum of Doctor Tarr and Professor Fether," that consists of a series of puzzles. These were later reprinted in the anthology, "The Lady or The Tiger? and Other Logic Puzzles." The last puzzle, which describes the asylum alluded to in the title, was designed to be especially difficult. With the help of automated reasoning, we show that the puzzle's hypotheses are, in fact, inconsistent, which is to say, no such asylum can possibly exist.

Large-scale Internet scans are a common method to identify victims of a specific attack. Stateless scanning like in ZMap has been established as an efficient approach to probing at Internet scale. Stateless scans, however, need a second phase to perform the attack, which remains invisible to network telescopes that only capture the first incoming packet and is not observed as a related event by honeypots. In this work, we examine Internet-wide scan traffic through Spoki, a reactive network telescope operating in real-time that we design and implement. Spoki responds to asynchronous TCP SYN packets and engages in TCP handshakes initiated in the second phase of two-phase scans. Because it is extremely lightweight it scales to large prefixes where it has the unique opportunity to record the first data sequence submitted within the TCP handshake ACK. We analyze two-phase scanners during a three months period using globally deployed Spoki reactive telescopes as well as flow data sets from IXPs and ISPs. We find that a predominant fraction of TCP SYNs on the Internet has irregular characteristics. Our findings also provide a clear signature of today's scans as: (i) highly targeted, (ii) scanning activities notably vary between regional vantage points, and (iii) a significant share originates from malicious sources., Comment: Proc. of 31st USENIX Security Symposium, camera-ready

In this paper, we revisit the open DNS (ODNS) infrastructure and, for the first time, systematically measure and analyze transparent forwarders, DNS components that transparently relay between stub resolvers and recursive resolvers. Our key findings include four takeaways. First, transparent forwarders contribute 26% (563k) to the current ODNS infrastructure. Unfortunately, common periodic scanning campaigns such as Shadowserver do not capture transparent forwarders and thus underestimate the current threat potential of the ODNS. Second, we find an increased deployment of transparent forwarders in Asia and South America. In India alone, the ODNS consists of 80% transparent forwarders. Third, many transparent forwarders relay to a few selected public resolvers such as Google and Cloudflare, which confirms a consolidation trend of DNS stakeholders. Finally, we introduce DNSRoute++, a new traceroute approach to understand the network infrastructure connecting transparent forwarders and resolvers., Comment: Proc. of ACM CoNEXT'21, camera-ready

In this paper, we present first measurements of Internet background radiation originating from the emerging transport protocol QUIC. Our analysis is based on the UCSD network telescope, correlated with active measurements. We find that research projects dominate the QUIC scanning ecosystem but also discover traffic from non-benign sources. We argue that although QUIC has been carefully designed to restrict reflective amplification attacks, the QUIC handshake is prone to resource exhaustion attacks, similar to TCP SYN floods. We confirm this conjecture by showing how this attack vector is already exploited in multi-vector attacks: On average, the Internet is exposed to four QUIC floods per hour and half of these attacks occur concurrently with other common attack types such as TCP/ICMP floods., Comment: Proc. of ACM IMC'21, camera-ready

In this paper, we shed new light on the DNS amplification ecosystem, by studying complementary data sources, bolstered by orthogonal methodologies. First, we introduce a passive attack detection method for the Internet core, i.e., at Internet eXchange Points (IXPs). Surprisingly, IXPs and honeypots observe mostly disjoint sets of attacks: 96% of IXP-inferred attacks were invisible to a sizable honeypot platform. Second, we assess the effectiveness of observed DNS attacks by studying IXP traces jointly with diverse data from independent measurement infrastructures. We find that attackers efficiently detect new reflectors and purposefully rotate between them. At the same time, we reveal that attackers are a small step away from bringing about significantly higher amplification factors (14x). Third, we identify and fingerprint a major attack entity by studying patterns in attack traces. We show that this entity dominates the DNS amplification ecosystem by carrying out 59% of the attacks, and provide an in-depth analysis of its behavior over time. Finally, our results reveal that operators of various .gov names do not adhere to DNSSEC key rollover best practices, which exacerbates amplification potential. We can verifiably connect this operational behavior to misuses and attacker decision-making., Comment: Proc. of ACM IMC'21, camera-ready