A. Voulimeneas
Please Note
33 records found
1
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.
...
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.
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. ...
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.
Witnessing Loops
Validating loop optimizations in LLVM through witnessing checking
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). ...
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).
MoveCast: An Atomic Multicast Protocol with Object Migration
Augmenting White-Box Multicast with the Shard Scheduler System
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. ...
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 Verificiation for Controllable Routing
Path Verification with Per-Hop Key Exchange Using Programmable Data Planes
Beyond the Exact Match
Investigating the Relationship Between Syntactic and Semantic Equivalence in Human and LLM Test Assertions
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. ...
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.
Can Small Beat Big?
Evaluating Fine-Tuned CodeT5 Models on Assertion Generation Quality and Efficiency
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. ...
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.
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%. ...
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%.
Machete
Thwarting Code-Reuse Attacks Through Temporal Permission Tightening in User-Space
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. ...
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.
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. ...
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.