AV

A. Voulimeneas

info

Please Note

33 records found

Open Radio Access Networks (O-RAN) offer a disaggregated, open alternative to the inflexible and monolithic design of current RAN architectures. The inherent result of the more open O-RAN architecture is an enlarged attack surface, making security a critical focus.

In this paper, the OpenAirInterface and OCUDU test beds, together with the FlexRIC and ORAN-SC near-RT RICs and the OAI-CN5G and Open5GS 5G core networks, are evaluated for vulnerabilities. By exploiting the unencrypted SCTP communications, it was possible to perform a masquerading attack that spoofs O-RAN components, a shutdown attack that injects shutdown messages to stop connections, and a heartbeat attack injecting heartbeat messages with malicious payloads into O-RAN connections.

The attacks found in this research, in combination with the characteristics of the SCTP protocol used in the O-RAN network, allow for the breaking of connections between O-RAN components internally, between network functions in the 5G core, and the near-RT RIC. The breaking of these connections triggers implementation vulnerabilities in the OpenAirInterface and OCUDU test beds, as well as the FlexRIC and ORAN-SC near-RT RICs. These vulnerabilities cause the components to crash or communications between them to be severed permanently.

To secure the O-RAN architecture, strict compliance with the O-RAN specification by implementing IPSec is necessary, together with robust error handling that can safely manage dropped connections and failed connection setup.
...
Rust's ownership-based type system provides strong memory-safety and aliasing guarantees, but unsafe Rust allows raw pointers to alias with references, which the static borrow checker cannot track. Dynamic aliasing models such as Stacked Borrows and Tree Borrows address this gap in the Rust interpreter Miri by defining when pointer uses create undefined behaviour. However, these models are implemented directly inside Miri, so changing or comparing model variants requires modifying the interpreter and risks semantic drift between model definitions and implementations. We present BorrowMIR, a model-parametric framework for specifying Rust aliasing models as explicit state-transition rules over MIR-level borrow events. BorrowMIR represents borrow state using per-location directed acyclic graphs with allocation-level metadata, allowing stack-shaped, tree-shaped, and more general alias derivation structures. From a single model specification, BorrowMIR generates a Rust backend for execution inside Miri and a TLA+ backend for trace checking, rule-merging validation, and structural invariant checking. We evaluate BorrowMIR by encoding Stacked Borrows, Tree Borrows, and smaller model variants. The generated full models match native Miri outcomes on the Miri borrow-tracker tests and selected Rust standard-library tests. Mutation testing detects 67 of 70 injected rule faults, and the BorrowMIR specifications are substantially smaller than the corresponding native implementations. Runtime overhead is the main limitation: generated Stacked Borrows is usable on the selected test suite, while generated Tree Borrows is considerably slower. Our results indicate that BorrowMIR supports the definition, execution, comparison, and bounded validation of Rust aliasing models outside Miri's native borrow-tracker implementation. ...
Master thesis (2026) - T. Kling, S.S. Chakraborty, Dennis Sprokholt, A. Voulimeneas
Translating programs between instruction sets is an unsolved problem. Memory op-
erations are strengthened to guarantee robustness of executions. Dynamic verification techniques from x86 to ARM currently do not implement the full ARM memory model. We show that dependence analysis on the source code can be used to prevent false positive robustness violations. We also show that it allows us to construct alternative executions to find violations involving po rf cycles, which previously could not be found. This solves the final limitations allowing dynamic memory translation from x86 to the full ARM memory model. ...

Validating loop optimizations in LLVM through witnessing checking

Master thesis (2026) - S.A. Mehmed, S.S. Chakraborty, A. Voulimeneas
Compiler optimizations improve program performance by transforming programs into more efficient yet semantically equivalent forms. However, ensuring the correctness of optimizations remains a challenge. Loops, in particular, often greatly increase a program's runtime. However, loop optimizations often significantly alter the underlying program structure, necessitating extensive verification. This work aims to extend an existing witnessing compiler framework with support for several loop optimizations. Overall, the findings demonstrate that a witnessing compiler is feasible to implement and can supplement transformations with an extra correctness guarantee. However, the complexity of constructing witness relations grows rapidly with the complexity of transformations themselves, and the current implementation incurs significant overhead. ...
Rust derives its memory-safety reputation from compile-time checks, but the binary the end-user runs only retains the subset of those checks that the compiler chose to emit at machine-code level. Once those emitted checks are present in the binary, they become a tampering target: an adversary with binary-modification access can neutralize the guard while leaving the unsafe operation in place. Detecting whether such a tampering has occurred presupposes a complete inventory of the compiler-inserted checks that should be there.

Prior work (EuroSec '24, Louka et al. 2024) demonstrates the feasibility of post-compilation tampering and locates checks structurally on stripped binaries, but its published inventory covers only the panic_bounds_check helper at a single optimization level, and its recall on stripped binaries is bounded by the function-boundary inference of the disassembler it builds on. No published locator categorizes checks by panic helper, or reports recall across all four standard optimization levels at a stripped-binary recall comparable to the unstripped case.

We present a locator that recovers compiler-inserted safety checks from stripped x86_64 ELF binaries using purely structural and control-flow features, no symbols, no string literals. A symbol-free helper-integrity pre-pass first fingerprints the build (link-time optimization or not) and checks the core panic-helper bodies; six phases then follow: structural panic-helper detection; compare-plus-branch recovery; signature and rule-based category classification; three-entry-point reachability tagging; depth-first orphan-region recovery; and an anomaly scan that flags compare sites whose guarding branch has been structurally broken. Each recovered check is annotated with one of twelve panic categories and with three reachability flags that distinguish checks on the execution-relevant call graph from dead-resident ones. The locator's output schema is designed to drive a companion validator that detects per-check tampering. Scope caveat: every category the locator emits corresponds to a spatial-safety check or to one of a small set of standard-library integrity checks that mirror them; non-spatial safety properties Rust enforces at the source level (aliasing discipline, ownership transfer, lifetime nesting) are discharged by the borrow checker at compile time, with two standard-library runtime exceptions (RefCell borrow guards and TLS liveness guards) that we deliberately exclude from the ground-truth scope and category vocabulary; non-spatial properties are therefore excluded from the locator's coverage claims.

On a corpus of 327 user-built Rust (binary, opt) inputs spanning four optimization levels plus the 18 EuroSec '24 paper binaries (345 inputs total, 134,536 ground-truth check pairs), the locator achieves a stable 94.3% loose recall across the four optimization levels and per-category recall at or above 89% on every panic category the standard rustc toolchain emits. At the per-check-identity level, individual safety checks are observed in only two states: either preserved with the same categorical signature (compare mnemonic, operand pattern, branch mnemonic) across optimization levels or dropped entirely, with no case of a check reshaped into a different signature. On a 1,500-sample tampering evaluation that auto-patches ground-truth check sites with five byte-level primitives (conditional-branch removal, branch redirection, signed-comparison substitution, immediate-value tampering, and operand-register substitution), the locator, run on the tampered binary alone, detects each tamper either by dropping the broken check from its output or by attaching a structural anomaly tag. The two structural primitives and the signed-comparison substitution are caught reliably (100%, 79.7%, and 100%), while the two operand-rewriting primitives that leave a valid-looking comparison are detected far less often (39.7% and 38.0%), a 71.5% pooled standalone detection rate; the remaining cases require the companion validator.

These results establish the structural locator as the high-recall first stage of a two-stage post-compilation tampering-detection system whose second stage is the companion validator. With the locator in place, the open question of which compiler-inserted safety checks are present in a deployed stripped binary, and which have been tampered with, can be answered on the binaries an end user actually runs. The contributions are both empirical (the recall and tampering numbers, on a larger corpus than the prior published evaluation) and methodological (the categorized (cmp, branch) output schema that the companion validator consumes to issue its per-check verdict). ...

Augmenting White-Box Multicast with the Shard Scheduler System

Bachelor thesis (2026) - R. Zaid, Jérémie Decouchant, A. Voulimeneas
Modern distributed systems, such as blockchains, rely on state partitioning (sharding) to achieve scalability, but transactions spanning multiple shards remain a major performance bottleneck that require expensive global coordination to preserve total ordering. While optimized atomic multicast protocols like White-Box significantly reduce communication latency, they do not inherently decrease the frequency of these costly cross-shard interactions. This thesis introduces MoveCast, a novel protocol that directly weaves dynamic object migration into White-Box atomic multicast to address this limitation. Utilizing a stop-restart mechanism, MoveCast temporarily freezes objects and migrates them to optimal shards, safely flagging any conflicting in-flight transactions for client retrial. We formally prove that MoveCast preserves the strict safety, ordering, and fault-tolerance guarantees of the original White-Box protocol. Furthermore, empirical evaluation using a custom Go simulator and a modified Sui blockchain dataset demonstrates significant performance gains. After an initial period of migrating objects to their ideal locations, MoveCast successfully reduced the cross-shard transaction ratio from 0.98 to 0.2, increased stable throughput from 3,800 to 4,850 transactions per second, and lowered average latency from 130 ms to 103 ms. ...
Credential database breaches cause substantial harm, yet the mean time to identify and contain a breach extends to 241 days on average, a window during which stolen credentials are exploited without the affected organisation's knowledge. Honeywords, decoy passwords stored alongside legitimate credentials, were proposed in 2013 as a low-cost mechanism to accelerate breach detection by raising an alarm when an attacker authenticates using a stolen credential, and have since attracted over 140 papers spanning twelve years of research. Despite this sustained effort, no empirical evidence of real-world honeyword deployment has been documented in the research literature. Unlike many security mechanisms whose adoption is simply unobserved, honeyword deployment leaves a structurally detectable signature in any leaked credential database, making the absence of evidence here empirically meaningful rather than merely anecdotal. This thesis presents the first empirical investigation into real-world honeyword deployment, structured around two questions: whether the technology has reached sufficient readiness for production deployment, and whether structural evidence of adoption is observable in leaked credential data. Deployment readiness is assessed through four independent signals: academic literature, patent filings, source code repositories, and a practitioner awareness sweep, including an actively instrumented pip-installable Django package, which collectively place honeyword technology at TRL 6. Deployment evidence is assessed through structural analysis of 487 server-side credential databases collected from dark web forums, spanning 11 industry sectors. Every breached service stores exactly one password digest per user account, with no post exhibiting a secrets-to-emails ratio at or above 2.0, the minimum any meaningful honeyword deployment would produce. This holds across all sectors and across 85 breaches attributable to the post-Amnesia period, after the primary architectural barriers had been addressed. The central finding is that the absence of honeyword adoption is not explained by low technology readiness, but by apparent practitioner unawareness, a coordination barrier that makes unilateral adoption economically unattractive, and additional operational and economic barriers that persist independently of architectural progress. ...
Master thesis (2026) - C. Perlog, G. Smaragdakis, A. Voulimeneas, R.E. Kooij, Ivo Kroskinski, Iker Olarra
Modern devices reveal their behavior through the network traffic they generate, yet widespread encryption has made payload inspection impractical and shifted the question from which application produced a flow to when the behavior of the device changes. This thesis studies how far behavioral transitions on a single networked device, such as switching applications or moving between foreground and background activity, can be detected from passive, encrypted traffic alone, using unsupervised concept drift detection that operates online and without labels.

The thesis contributes an end-to-end pipeline that turns raw packet captures into windowed feature streams, four labeled recordings collected on dedicated Android and iOS test devices, and an empirical comparison of seven streaming change detectors under realistic observability constraints. It proposes Online NN-DVI, a streaming density-based detector, together with a retro-confirmation segmenter that converts raw detector alarms into labeled behavioral segments online.

Across the four recordings and an external cross-corpus check on the public Mirage dataset, density-based detectors are the most effective paradigm, and Online NN-DVI matches the offline NN-DVI baseline within a few F1 points at roughly an eighth of its runtime, generalizing from a single tuning recording to held-out Android, iOS, and Mirage data without per-dataset retuning. Detectability is gated by the type of transition: app-to-app foreground switches are caught in roughly two thirds of cases, foreground enter and exit transitions in about one in three, and administratively defined idle boundaries not at all. An 18-feature behavior subset matches a 54-feature candidate set, and 5-second window aggregation outperforms 1-second aggregation on both accuracy and runtime, while the segmenter reaches a frame-level F1 of 0.739. Taken together, the results indicate that what limits detection on this stream is the signal carried by the features, not the algorithm operating on them. ...

Path Verification with Per-Hop Key Exchange Using Programmable Data Planes

Modern Internet routing gives end users little control over the paths their packets take and little evidence that packets followed an intended route after transmission. Although routing protocols such as BGP determine reachability at Internet scale, they do not provide packet-level guarantees that traffic traversed a chosen set of routers or avoided untrusted network regions. This gap is increasingly relevant for use cases involving regulatory compliance, data-residency requirements, security-sensitive communication, and post-incident forensic analysis. Existing approaches to path validation and source-controlled routing either require clean-slate deployment, rely on cryptographic primitives that are too expensive for programmable data planes, or introduce per-hop header overhead that grows with path length. This thesis investigates whether controllable packet forwarding can be combined with lightweight cryptographic path verification in programmable data planes. It presents Hermes, a prototype system that allows a sender to route packets through an ordered set of trusted switches and later verify that the packet traversed exactly that path. Hermes uses a compact in-band accumulator carried in each packet. Each switch on the authorised path shares a pool of secret keys and opcode assignments with a central Hermes server. As a packet passes through a switch, the switch applies a keyed operation to the accumulator using only P4-compatible arithmetic and bitwise operations. The receiver emits the resulting accumulator to the control plane, after which the Hermes server independently replays the computation and returns an "Accept" or "Reject" verdict. The design avoids data-plane AES, HMAC, modular exponentiation, and other primitives that are difficult to express in a P4 match-action pipeline. Instead, Hermes uses an optical Diffie--Hellman variant based on XOR and AND operations to provision per-switch key material, and a Galois Linear Feedback Shift Register (LFSR) to drive key-index selection after the initial key pool has been consumed. Replay protection is provided through per-flow sequence numbers, millisecond-resolution timestamps, and server-issued nonces. The prototype is implemented using P4, Python, and C++, and evaluated through a set of experiments measuring key-exchange latency, end-to-end verification latency, throughput and loss behaviour, key-rotation overhead, path-deviation detection, and header overhead. The evaluation shows that Hermes can perform key provisioning within millisecond-scale latency, verify packets with low and stable end-to-end latency across the tested probe rates, and detect the evaluated path-deviation and replay scenarios with perfect accuracy in the experimental setup. The protocol introduces a fixed per-packet header overhead rather than overhead that grows with path length. The security analysis shows that the accumulator construction provides practical path-integrity evidence under the stated threat model, but also identifies important limitations: repeated observations under key reuse remain the dominant source of cryptanalytic risk, the 32-bit accumulator limits the strength of the construction, and the key-exchange channel must be protected in a production deployment. Overall, Hermes demonstrates that programmable data planes can support a lightweight form of controllable and verifiable routing without relying on heavyweight cryptography in the forwarding path. The system should not be interpreted as a replacement for full Internet-scale architectures such as SCION or ICING; rather, it shows that switch-level path verification is feasible as an incremental building block for more accountable network infrastructures. ...
Unit test assertions are essential for detecting software faults, yet writing them remains costly and time-consuming. Large Language Models (LLMs) offer a promising way to automate assertion generation. However, prior work has primarily focused on generating assertions that closely mimic human-written ones. Because this represents only one possible generation strategy, the impact of alternative approaches on overall quality remains poorly understood. This paper presents an empirical study evaluating four distinct generation strategies: Assertion Generation, which was proposed and evaluated in prior work, alongside Assertion Augmentation, Blind Augmentation, and Chain-of-Thought Generation. Using GPT-oss 20b as the underlying model, we evaluate these strategies on 811 test oracles from 10 open-source projects in the GitBug-Java benchmark. We assess the generated assertions in terms of correctness, fault-detection capability, and textual similarity to developer-written assertions. Our results show that the choice of generation strategy strongly influences performance. Assertion Augmentation performs best overall, achieving the highest compilation rate, execution validity, and mutation score. Meanwhile, Chain-of-Thought Generation detects the highest proportion of real bugs, and standalone Assertion Generation yields results most similar to developer-written tests. Overall, the findings demonstrate that providing LLMs with existing developer-written assertions substantially improves the quality and effectiveness of generated test oracles. ...
Testing software is essential for verifying that software is correct and behaves as intended. Large Language Models (LLMs) have shown promise in generating effective test oracles, which are defined as the mechanism used to determine the correctness of the behaviour for a given input to a System Under Test (SUT). Prior work has shown that the type of context provided to an LLM influences the quality of generated oracles. However, existing work often evaluates these oracles by comparing them to human-written assertions, which may not fully reflect real-world oracle quality. This paper investigates how different configurations of context types influence the quality of LLM-generated test oracles. We replicate prior work by evaluating eight context configurations using more realistic quantitative quality measures, including compilation rate, pass rate, mutation score, and test strength. Furthermore, we extend this evaluation by investigating whether compressed context can retain enough relevant information to generate useful oracles. The results suggest that including the focal class improves the quality of LLM-generated assertions the most among the evaluated context types. The effect of Javadoc is mixed: it improves results when available code context is limited. However, its effect is limited or even negative when richer code context is already available. Compression methods effectively reduce the number of tokens, but do not retain the full quality of the generated test oracles. The uncompressed configuration performs best overall. However, when context size is important, the test prefix paired with a summary provides a reasonable trade-off between oracle quality and token usage. ...

Investigating the Relationship Between Syntactic and Semantic Equivalence in Human and LLM Test Assertions

Test assertions form a critical component of software tests, as they are the component that actually verifies whether the code under test is exhibiting the desired behaviour. However, writing test assertions is time consuming, and thus research has been carried out on how to help in automation of this task. Since the emergence of Large Language Models (LLMs) in recent years, interest in their application for assertion generation has grown. LLMs have shown promise, with LLM-generated assertions achieving mutation scores similar to human-written assertions. However, existing research evaluates the assertions based on either exact matches or mutation scores in isolation, thus not investigating the relationship between syntactic and semantic equivalence. This matters because syntactically different assertions can have the same semantics. Punishing the LLM for writing assertEquals(a, b) instead of assertTrue(a.equals(b)) leads to systematically under-reported LLM performance.

In this paper we investigated the extent to which LLM-generated assertions differ syntactically but remain semantically equivalent to human-written reference assertions. We construct a dataset with 177 filtered entries drawn from open source projects and generate assertions using gpt-oss-20b. We then measure the syntactic similarity via normalised tree edit distance and related metrics. We approximate the semantic similarity based on Jaccard and Ochiai similarity between the sets of mutants killed with PIT mutation testing. We find a moderately strong correlation between normalised tree edit distance and the Jaccard similarity of the killed mutants (ρ = -0.685, p < 0.001), indicating that the two metrics are related but not interchangeable. Open coding of 41 semantically equivalent but syntactically different pairs revealed ten transformation categories. The LLM showed a universal preference for the omission of assertion messages and for replacing boolean checks with equality assertions. We use open coding to evaluate the syntactic differences between semantically equivalent assertions. Finally we use a decision tree to generate a threshold allowing us to effectively distinguish between datapoints likely and unlikely to be semantically equivalent. We find this threshold to be 0.41 for the normalised tree edit distance, showing a median Jaccard similarity of 0.5290 below it and a median of 1.000 above it. Our findings suggest that exact match evaluation significantly underestimates LLM assertion generation performance, and that syntactic similarity with a fixed threshold offers a more useful metric for assertion quality. ...

Evaluating Fine-Tuned CodeT5 Models on Assertion Generation Quality and Efficiency

Testing is a core practice in software development for detecting faults and checking that code behaves as expected. With the recent advent of Large Language Models (LLMs), code generation has never been more widespread. In assertion generation, where the focus is on the oracles that assess the state of the program, fine-tuned code language models have emerged. One such model, AsserT5, is a CodeT5-large (770M parameters) fine-tuned on focal-method and test-method pairs. Although it achieves state-of-the-art performance when measured by exact match to the ground truth, it remains unclear how the top-1 predictions of the smaller variants (CodeT5-small, 60M; CodeT5-base, 220M) perform on mutation score when the same fine-tuning procedure is applied.

Across ten real-world Java projects and 541 assertion-generation tasks, we find that the fine-tuned 60M CodeT5-small matches the 220M and 770M variants on mutation score (within 0.2 p.p.), achieving the highest score of the three by generating more assertions that compile. Among the larger code-specific baselines (Qwen2.5-Coder 3B, 7B, and 14B), CodeT5-small underperforms only the 14B model, and only by 0.6 p.p. This advantage is concentrated in just two of the ten projects, and the 14B model attains it at the cost of 38x more memory (9.00 GB vs 0.24 GB) and 2.6x slower inference. Because the difference is small and confined to two out of ten projects, we recommend the fine-tuned CodeT5-small to practitioners seeking local assertion-generation assistance at reasonable computational cost. ...
Atomic multicast enhances Decentralized Finance scalability by partitioning networks into shards that operate in parallel, effectively reducing messaging complexity. However, a critical issue remains: the fair sequence of cross-shard transactions is not strictly guaranteed. A leading cross-shard protocol, Haechi, treats each shard as a black box, resulting in an architectural blind spot regarding unequal mempool delays across shards. Exploiting this, we formalize a novel cross-shard mempool front-running attack. By modeling bounds on congestion latency and network routing, we mathematically prove this attack succeeds whenever an adversary’s routing overhead is strictly less than the mempool delay difference between shards. We propose replacing Haechi’s block-based timestamping with per-transaction entry timestamping, neutralizing the effects of localized congestion. The timestamp integrity is secured by a modified Quorum Certificate (QC) mechanism, and transactions are strictly sequenced through a novel Minimum-Barrier Sorting protocol. While this structural mitigation successfully preserves horizontal sharding efficiency, enforcing strict cross-shard fairness introduces an inevitable trade-off: reducing transaction liveness and requiring a partially synchronous network. ...
Asymmetric Byzantine Quorum Systems (ABQS) generalize classical distributed consensus by allowing individual processes to maintain subjective, heterogeneous trust assumptions. While foundational primitives like reliable broadcast and consensus have been established in this model, higher-level multi-group communication abstractions remain unexplored. This paper presents the first partially genuine atomic multicast protocol for the ABQS model by adapting the ByzCast architecture. We demonstrate that applying the classical Chandra-Toueg reduction to existing asymmetric primitives yields an atomic broadcast implementation with stronger safety guarantees than existing alternatives, extending correctness to all wise processes rather than confining it to the maximal guild. Our adapted multicast protocol preserves partial genuineness, ensuring that single-group messages only require coordination within their target destination. Empirically, we evaluate the protocol's liveness resilience through robustness experiments. The results demonstrate a fundamental trade-off: while completely arbitrary trust profiles make atomic multicast difficult to sustain under faults, the natural clustering observed in decentralized networks significantly flattens failure curves and recovers system viability. ...
This thesis studies the correctness of compiling the Java Memory Model to Armv8. We identified and corrected an issue in the JAM-21 definition of corw and then present a performant mapping from Java access modes and fences to Armv8 instructions that avoids unnecessary barriers. The correctness of this mapping is formally verified in Rocq by adapting the IMM proof structure. The proof shows that Arm-consistent executions remain Java-consistent under the corrected model, covering the key coherence components of the Java memory model. ...
The successive generations of consensus algorithms progressively shifted the performance bottleneck of blockchains to the execution layer. Recent works have addressed this bottleneck by parallelizing the execution of transactions. Historically, transaction ordering was left to the discretion of validators, a practice that lacked transparency and gave rise to Maximal Extractable Value (MEV) attacks where transaction ordering is manipulated for private gain. More recently, the focus has shifted toward fair ordering protocols that prioritize chronological submission. However, fair ordering is often misaligned with validator incentives and negatively impacts execution throughput under high congestion. In this work, we address the tension between validator revenue and fair ordering using a dynamic optimization framework.

We define a blockchain-independent model to evaluate transaction ordering in a continuous setting where the execution of successive blocks can overlap. Within this model, we propose an anytime genetic algorithm. We use real-world blockchain data and execution time estimates within realistic error margins, showing that this approach increases validator profit by around 15% and accelerates congestion relief. We also quantify the impact of adding fair ordering constraints on validator revenue during congestion, showing that revenue decreases by around 50%. ...

Thwarting Code-Reuse Attacks Through Temporal Permission Tightening in User-Space

Modern software ships with substantial unused code. Dynamic linking loads entire shared libraries when only a fraction is required, features accumulate over release cycles, and one-size-fits-all distribution models ship complete binaries regardless of deployment context. This bloat directly expands the attack surface available to adversaries: unused but mapped code provides gadgets for return-oriented programming (ROP) and jump-oriented programming (JOP) attacks. Existing defenses are partial. Address space layout randomisation is defeated by memory-disclosure vulnerabilities. Execute-only memory prevents reading code pages but does not reduce their volume. The W⊕X policy prevents code injection but not code reuse.

Software debloating removes unused code, but existing tools face trade-offs between source access, soundness, precision, and deployment requirements. Binary-level tools such as Razor operate only on the application binary and leave shared libraries fully mapped. Static-analysis tools such as Decker are conservative in their approximation and likewise skip library code. Kernel-level mechanisms can achieve strong isolation but require kernel modifications that limit deployment. No existing system combines temporal restriction, where different code is accessible at different stages of execution, with execute-only memory enforcement over the full dependency chain in user space.

We present Machete, a software debloating framework that derives temporal memory-access policies from execution traces and enforces them entirely in user space, without kernel modifications or source code access. Machete operates in three stages. A segfault-based profiler captures page-granularity access patterns for both single- and multi-threaded programs. A modified Blue-Fringe/EDSM learner infers a phase-structured finite-state machine from these traces, with tunable scoring coefficients that control the security/performance trade-off. An enforcement runtime then runs each phase in a separate operating-system process with its own page-table permissions and execute-only memory over shared physical memory, debloating the full dependency chain, including shared libraries.

We evaluate Machete against Razor and Decker on 11 shared targets and 2 auxiliary multi-threaded targets. Machete reduces executable pages by 86 to 95% from the original binary; even the worst-case phase exposes 2 to 5 times fewer pages than both Razor and Decker. ROP gadgets drop by 33 to 78% per phase, and all enforced variants have zero readable-executable application pages, preventing runtime gadget discovery. For CPU-bound workloads, enforcement overhead is below 4%. For server workloads, overhead ranges from 2.7% (memcached) to 66.6% (lighttpd), depending on phase-transition frequency, and a parameter sensitivity analysis confirms that the operator can navigate this trade-off through stable regions in the scoring-coefficient space. Machete is, to our knowledge, the first system to combine temporal debloating of executable pages with execute-only memory enforcement in user space. ...
Master thesis (2025) - M.S. Patil, A. Katsifodimos, A. Voulimeneas
While database systems have matured significantly over the past few decades, the rapid growth of real-time analytics to feed quick decision making has paved a way for multipurpose and high performant systems. As stream processing also matures, it is of interest to explore its full functional capabilities such as state management. Most streaming systems have inaccessible state for external systems to query, which limits the ability to drive value from the live mutable state data. In this thesis we present Q-Styx, a system that exposes the live state of stateful operators in a streaming engine for external queries. We introduce a global state store that maintains a copy of the distributed state across the system without the need of an external database. With strong isolation guarantees for consistent results, our implementation balances the tradeoffs between performance isolation and data freshness while exhibiting minimal impact on the core transactional capabilities of the streaming engine. ...
Master thesis (2025) - M.A. Mladenov, G. Smaragdakis, Robert Beverly, Taha Albakour, Jérémie Decouchant, A. Voulimeneas
The Border Gateway Protocol (BGP) is the Internet's de facto inter-domain routing protocol. Due to its critical role in backbone infrastructure, denial of service attacks on BGP routers have the potential to compromise global connectivity.

BGP is not a standalone protocol; it relies on other protocols such as the Transport Control Protocol (TCP). In this work, we research whether BGP's reliance on TCP could lead to vulnerabilities allowing non-peers to perform denial of service attacks. We develop a methodology allowing researchers, vendors, and operators to enumerate potential weaknesses or vulnerabilities in routers and propose three attack types. We apply this methodology to physical and virtual routers from three popular vendors and identify several potential vulnerabilities. We find that one vendor's BGP implementation is susceptible to two types of attacks: SYN Flood and Connection Exhaustion. They allow a remote non-peered attacker to stop legitimate peers from connecting to the BGP listener of the affected router, preventing the exchange of routes. We responsibly disclose the vulnerability to the affected vendor. Our results show that as few as 5 to 20 packets per second can be sufficient to perform denial of service. Finally, we propose several ways to mitigate the impact of the proposed attacks. ...