arXiv subjects

David Knothe

Publications and source records attributed to David Knothe.

2 recordsLinked to original sources

arXiv2026

Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations

Verified compilers aim to guarantee that compilation preserves the observable behavior of source programs. While small-step semantics are widely used in such compilers, they are not always the most convenient framework for structural transformations such as loop optimizations. This paper proposes an approach that leverages both small-step and big-step semantics: small-step semantics are used for local transformations, while big-step semantics are employed for structural transformations. An abstract behavioral semantics is introduced as a common interface between the two styles. Coinductive big-step semantics is extended to correctly handle divergence with both finite and infinite traces, bringing it on par with the expressiveness of small-step semantics. This enables the insertion of big-step transformations into the middle of an existing small-step pipeline, thereby fully preserving all top-level semantic preservation theorems. This approach is practically demonstrated in CompCert by implementing and verifying a few new loop optimizations in big-step Cminor, including loop unswitching and, notably, full loop unrolling.

cs.PL↗

arXiv2019

Large-Scale-Exploit of GitHub Repository Metadata and Preventive Measures

When working with Git, a popular version-control system, email addresses are part of the metadata for each individual commit. When those commits are pushed to remote hosting services like GitHub, those email addresses become visible not only to fellow developers, but also to malicious actors aiming to exploit them. As a part of our research we created a tool that leverages the publicly available GitHub API to collect user data. Analysis of this data not only gives access to millions of email addresses in very little time, but is also powerful and dense enough to create targeted phishing attacks posing a great threat to all GitHub users and their private, potentially sensitive data. Even worse, existing countermeasures fail to effectively protect against such exploits. As a consequence and main conclusion of this paper, we suggest multiple preventive measures that should be implemented as soon as possible. We also consider it the duty of both companies like GitHub and well informed software engineers to inform fellow developers about the risk of exposing private email addresses in Git commits published publicly.

cs.CR↗