Student Blog

Formal specifications play a pivotal role across the entire lifecycle of complex systems, beginning with the design phase where they establish unambiguous and rigorous requirements. These specifications continue to be indispensable in the operational phase, where they enable the automation of intricate tasks such as monitoring and anomaly detection. However, formal specifications are often unavailable or challenging to define, underscoring the significance of specification mining techniques that can automatically infer specifications from system executions. Until now, existing specification mining methods have focused on learning properties defined over single system executions, while hyperproperties, which extend properties by establishing relationships across multiple distinct executions, have been neglected due to their greater complexity. Consequently, many relevant system characteristics, such as robustness or security policies, could not be learned from data.

With our paper, we filled this gap in the literature. By combining insights from the program synthesis research field with established parameter learning methods, we also proposed the first mining approach that allows the user to regulate the amount of knowledge to embed in the process. The outcome is a surprisingly flexible method applicable in a plethora of applications from different domains.

In existing literature, the concept of decomposing path error into two components is well-established. One component tracks path progression tangentially, while the other quantifies deviations from the path in an orthogonal direction. This approach has traditionally been applied to position control. In our work, we extend this concept to orientation control, leveraging the principles of Lie theory for rotations. Additionally, we introduce a method to partition the orthogonal error plane into basis directions, simplifying the definition of asymmetric Cartesian error boundaries. Employing piecewise linear position and orientation reference paths, our approach is computationally efficient and allows real-time trajectory adjustments during the robot’s motion. This adaptability empowers our planner to excel in dynamic environments or when the robot faces new objectives.

BoundMPC has undergone testing with a robot in two distinct scenarios. In the first scenario, the robot maneuvers a large object through a confined space, involving tilting maneuvers. In the second scenario, the robot retrieves an object from a table while avoiding collisions with nearby obstacles.

Video

I introduced Glimpse, a groundbreaking cross-chain communication protocol designed for PoW blockchains. What sets Glimpse apart is its ability to simultaneously achieve security, practicality, efficiency, and compatibility with a wide range of chains, all while offering enhanced expressiveness. Specifically, Glimpse ensures atomicity by only verifying and storing on the destination chain a constant amount of data relative to the source chain’s length. This results in minimal on-chain costs, making it accessible even to chains with limited scripting language capabilities.

Furthermore, Glimpse opens the door to a multitude of real-world applications within the DeFi sector. These include cross-chain lending, Proofs-of-Burn, token wrapping and unwrapping, as well as off-chain applications. Glimpse, in essence, represents a significant advancement in cross-chain communication protocols, enabling a wide range of innovative possibilities within the blockchain ecosystem.

Starting from the idea of Glimpse, we have now designed Blink, a new provably secure super-light client, which allows to read the state of a PoW blockchain efficiently, securely, and trustlessly. This makes Blink the perfect tool for applications such as wallets, which read the current state of the chain in order to let users know their account balance.

In the future, my aspirations include developing bridges for Proof-of-Stake blockchains.

Botnet detection remains a challenging task due to many botnet families with different communication strategies, traffic encryption, and hiding techniques. Machine learningbased methods have been successfully applied, but have proven to be vulnerable to evasion attacks. We show how an attacker can evade the detection of botnet traffic by manipulating selected features in the attack flows. We first build two well-performing machine learning models - Random Forest and Support Vector Machine - trained using only features available in encrypted traffic. We then show with two different data sets how the detection rate (recall) decreases significantly for both models if only a few basic features are manipulated by the attacker. We apply two state-of-the-art evasion attacks: Hop Skip Jump and Fast Gradient Sign. For all manipulated attack vectors we perform a plausibility check to ensure consistency with traffic statistics and protocol rules as well as a bot check to ensure the manipulated attack vectors are still valid bot samples.

Our research demonstrates that the machine learning algorithms can easily be fooled if the attacker is able to test the black-box models numerous times. Since in a real setting, attackers may not have access to the model and training data, we investigate if the generated attack samples are transferable to other machine learning models trained with different training data. Our results show, that samples generated with Hop Skip Jump generally do not transfer well to other models while Fast Gradient Sign samples generally also evade the detection of models different from the one they were customized for.

This manual process may overlook logical flaws for two main reasons. First, web specifications are usually very large and informally specified. Second, Web components are mostly evaluated in isolation without considering their composition and possible interactions. For this reason, we developed WebSpec, a framework for the formal analysis of browser security mechanisms allowing for the automated discovery of logical flaws and the development of machine-checked security proofs.

WebSpec includes a comprehensive model of the web browser in the Coq proof assistant, the formalization of 10 Web security invariants, and a toolchain to enable model checking with the Z3 theorem prover. If Z3 discovers a violation, WebSpec generates executables tests that can be validated across all major browsers. In this work, we discover two new logical flaws and verify the correctness of our proposed changes to the Web platform.

Existing methods of verification focus on a very limited property (local robustness) of neural networks. We have set out to give a better solution to this by designing a generalized method for neural network verification which gives stronger guarantees and is more expressible by using hyper-properties. Our approach will help ensure that neural networks are utilized in the best way possible eradicating the current concerns that come with them.

In our publication SMT Solving over Finite Field Arithmetic we present one of the first automated decision procedures for formulas over finite field polynomials. We utilize well-proven SMT solving techniques to craft a novel SMT theory for finite field polynomials to be used by future verification endeavors for zero-knowledge proof applications.

Protocols are ubiquitous in our digitalized life, we rely on them for almost everything from authenticating to our wifi router, to exchanging data with most websites. However, they are famously error-prone in design. For instance, previous versions of the TLS protocol (used to secure communication on the web) were repeatedly broken. Hence a strong need for computer-verified proofs. And, why not, fully automated protocol verification?

Many battle-tested tools already exist to tackle this problem (most famously ProVerif and Tamarin). Most of them, however, work within a model that (mostly) underestimates the capabilities of a real malicious agent. We set out to fix this flaw by designing an automated protocol verifier sound against the real-world attacker. Limited automation in this model already exists with the tools EasyCrypt and CryptoVerif. Our tool reasons with the so-called BC-logic (from the name of its creators: Gergei Bana and Hubert Comon-Lundh), which gives us a more automation-friendly approach than previously existing solutions. This lets us do symbolic proofs and rely on existing efficient first-order theorem provers to derive computational results.

Ethereum is currently the most important distributed ledger technology (blockchain) for DeFi services. It differs from the Bitcoin blockchain conceptually as it implements the so-called “account model” with two different account types. An externally owned account (EOA) is a “regular” account controlled by a private key held by some user. A code account (CA), which is synonymous with the notion “smart contract,” is an account controlled by a computer program, which is invoked by issuing a transaction with the code account as the recipient. In our analysis, we want to understand and discover relations between DeFi protocols and associated CAs. For that purpose, as shown in Figure, we constructed networks consisting of DeFi traces on two abstraction levels: the lower-level DeFi Code Account (CA) network and the higher-level DeFi Protocol network.

Our research began by gathering data from 23 DeFi protocols and their 10,663,881 associated Ethereum accounts to analyze their interactions based on transactions data from Ethereum. From a network perspective, we observe a high degree and centrality of decentralized exchanges and lending protocols, with interactions primarily occurring within a strongly connected component between them. Notably, traditional community detection methods proved insufficient for disentangling these interactions.

To address this challenge, we propose an innovative algorithm designed to decompose the building blocks of DeFi protocols within single transactions. Our findings reveal that these building blocks can be nested, illustrating how components of DeFi protocols interconnect in complex structures across multiple protocols.

To demonstrate the practicality of our approach, we present a case study inspired by the recent collapse of the UST stablecoin in the Terra ecosystem. Under the hypothetical assumption of a similar fate for the USD Tether stablecoin, we investigate which DeFi protocols would be affected and examine their dependencies on USD Tether. In summary, our results and methodologies contribute to a deeper understanding of this emerging family of financial products.

By automating feature extraction for heterogenous file types, providing reliable datasets and employing state-of-the-art clustering techniques, our work serves as a source of stimulation for future research in this critical field. Attribution of Diverse APT empowers security practitioners with automated tools to enhance attribution analysis and evaluate APT samples’ origins, advancing the cybersecurity practices.

Combining these two language features is notoriously difficult, and impossible to achieve in a complete way. In our paper we introduce an algorithm that combines these two features that gives strict guarantees about what we can prove and that out-competes all the state of the art algorithms in this area.

The calculus we introduce can deal with very general problems that contain arithmetic, quantifiers and uninterpreted functions, which means it can be used for a large number of problem domains, like verifying the correctness of soft and hardware systems, or proving security thereof.

In contrast to SAT solvers, the constraints in SMT do not necessarily include only Booleans (true or false), but possibly also “theory variables and theory constraints”. These theories may be, for example, integers or real (e.g. Find some “x” and “y” out of the positive integers such that x + 2y < y * y ∧ x / y > y) but can be also more exotic ones like partial orders or sequences. The high efficiency of SMT solvers relies on sophisticated decision procedures for the supported theories and their operators (such as +, *, <). Until now, if no decision procedure is built in, users either had to use quantifiers to model the theories themselves, which usually results in very poor performance and non-termination, or they had to modify the solver’s code base, which is quite cumbersome and requires deep knowledge of the solver’s internals.

We introduced the so-called “user-propagation” framework in Z3, one of the leading SMT solvers. It allows its users to implement their own domainspecific decision procedures for new theories, as well as heuristics and lazy formula encodings, directly in Z3 without having to recompile the solver or deal with implementation details of Z3. This can be achieved by providing a handful of (optional) event handling functions (see Figure) that are called by Z3 during reasoning as soon as a potentially relevant event occurs. These functions can return additional information and hints to the solver in these cases (e.g. conflicts or branching suggestions). We have shown that we can easily outperform “Vanilla Z3” in terms of memory usage and reasoning time by providing only a few (self-programmed) problem-specific functions. This way, we can solve even more problems via SMT reasoning that could not be solved before.

In our recent paper published at QEST 2022, we were able to lift this restriction and provide a solution to compute moments of probabilistic loops that were considerably beyond the state-of-the-art. Our approach combines recently established techniques from program analysis with the mathematical method of polynomial chaos expansion. Many real-world systems, such as autonomous vehicles, can only be modeled using general non-polynomial functions. Our paper opens the door for the automatic and exact analysis of such systems to make them safer.

Our paper proposes a hybrid Holochain and Blockchain-based privacy perseverance and security framework for IoT-HSs that combines the benefits of both technologies, overcoming computational, memory, and authentication challenges. This framework is particularly well-suited for IoT scenarios where resource optimization is essential. A comprehensive security and performance analysis is conducted to demonstrate the suitability and effectiveness of this hybrid security approach for IoT-HSs compared to Blockchairi-only or Holochairi-only based approaches.

The framework introduced in this work breaks new ground by combining two prominent technologies, Holochain and Blockchain, in an innovative way, offering significant improvements over conventional approaches to IoT security. Holochain helps reduce storage capacity requirements, while Blockchain ensures data integrity and security during data transfer among legitimate users. This framework enhances data security and efficiency, holding significant relevance across various IoT applications, from the industrial sector to healthcare. In the healthcare sector, it effectively addresses critical challenges related to patient data confidentiality, integrity, and real-time data processing. These contributions improve the overall reliability and trustworthiness of IoT networks, making them more suitable for critical healthcare applications.

In our paper, we developed a new exact algorithmic technique to compute the expected values of variables in probabilistic loops. Loops are the most challenging aspects of the automated analysis of programs. Our technique is based on the theory of recurrences and is able to analyze stochastic systems from many different areas.

We’ve rigorously tested our methods in various scenarios, such as analyzing financial decisions and studying the movement of objects in unpredictable environments. Our findings consistently demonstrate the high accuracy and reliability of our predictions. This approach stands out as superior to current practices in the field.