Events

2025-04-28 Research Seminar
String Solving via Extended Nielson Rules

2025-05-12 Research Seminar
ALASCA: Reasoning in Quantified Linear Arithmetic

2025-06-02 Research Seminar
Advancing the Security of Leaky Hardware

2025-04-07 Research Seminar
Securing Distributed Hash Tables using Proofs of Space

2025-04-03 Distinguished Lecture
Lecture by Grigory Fedyukovich (Florida State University) “Maximizing Branch Coverage with Constrained Horn Clauses“

Location: TU Wien , EI 4 Reithoffer HS (Haupttrakt, Gußhausstraße 25-25a, 2. Stock) (CF0245 )
Date/Time: 2025-04-03 15:00 ‒ 16:00

Abstract: State-of-the-art solvers for constrained Horn clauses (CHC) are successfully used to generate reachability facts for software using its symbolic encoding. In this talk, I will present a new application of CHCs to test-case generation, a problem of finding a set of tuples of input values to a program under which the program visits as many branches as possible. The key insight to achieve maximality is to identify and skip blocks of code that are provably unreachable. The new approach to test case generation called HORNTINUUM uses CHC to construct different program unrollings incrementally and extract test cases from models of satisfiable formulas. At the same time, a CHC solver keeps track of CHCs that represent unreachable blocks of code, making the unrolling process more efficient. In practice, this lets HORNTINUUM terminate early while guaranteeing maximal coverage. HORNTINUUM exhibits promising performance: it generates high coverage in most cases and takes less time on average than state-of-the-art based on bounded model checking, concolic execution, and/or fuzzing.

Bio: Grigory Fedyukovich is an Assistant Professor at Florida State University. He completed his Ph.D. at the University of Lugano under the supervision of Prof Natasha Sharygina, a postdoc at the University of Washington with Prof Rastislav Bodik, and a postdoc at Princeton University with Prof Aarti Gupta. His main research interests are in the fields of automated reasoning, software verification, and synthesis.

2025-03-17 Award
Barbara Gigerl received her doctorate sub auspiciis, a recognition for exceptional academic achievements, under the auspices of the Federal President of the Republic of Austria

Barbara Gigerl from TU Graz received her doctorate under the auspices of the President of the Republic (Promotio sub auspiciis Praesidentis rei publicae) in recognition of her exceptional achievements in both school and university. The graduation ceremony , performed by Peter Riedler, Rector of the University of Graz, and Horst Bischof, Rector of Graz University of Technology (TU Graz), took place on Friday, 14 March 2025, in the Great Hall of the Old University of Graz. Subsequently, Federal President Alexander Van der Bellen personally presented the Ring of Honour featuring the Federal Eagle of the Republic of Austria to the graduates at a reception in the Vienna Hofburg on 17 March 2025. This event celebrates her outstanding academic accomplishments.
Thesis

2025-03-17 Research Seminar
Towards a Composable Game-Theoretic Framework for Blockchains

2025-03-10 Research Seminar
SnailLoad: Exploiting Remote Network Latency Measurements without JavaScript

2025-03-10 Distinguished Lecture
Maria Eichlseder delivered a lecture at the Cluster of Excellence CASA

Maria Eichlseder presented Automated Tools for Symmetric-Key Cryptanalysis at the Spring School on Symmetric Cryptography .

2025-03-06 Outreach to society.
Austria’s largest education fair BeSt

Martina Lindorfer joined the TU Wien team at BeSt, the prominent education fair, where they showcased the university’s diverse degree programs. Alongside other team members, she represented ongoing research in security and privacy at TU Wien. She engaged with attendees, answering questions and providing a hands-on look at what studying Computer Engineering at TU Wien involves.

2025-03-04 Distinguished Lecture
Lecture by Jonathan Katz (Google) “Round-Optimal Fully Secure Distributed Key Generation“

Abstract: Protocols for distributed (threshold) key generation (DKG) in the discrete-logarithm setting have received a tremendous amount of attention in the past few years. Several synchronous DKG protocols have been proposed, but most such protocols are not fully secure: they either allow corrupted parties to bias the key, or are not robust and allow malicious parties to prevent successful generation of a key.
We explore the round complexity of fully secure DKG in the honest-majority setting where it is feasible. We show the impossibility of one-round, unbiased DKG protocols (even satisfying weaker notions of security), regardless of any prior setup. On the positive side, we show various round-optimal protocols for fully secure DKG offering tradeoffs in terms of their efficiency, necessary setup, and required assumptions.
Video Paper
Bio: Jonathan Katz recently joined Google as a Senior Staff Research Scientist, after more than 20 years as a professor at the University of Maryland where he also served as director of the Maryland Cybersecurity Center. He is a co-author of the widely used textbook “Introduction to Modern Cryptography” (now in its third edition) and also offers a free online course on cryptography through Coursera. Katz has received an Alexander von Humboldt Research Award, a UMD Distinguished Scholar-Teacher Award, and an ACM SIGSAC Outstanding Contribution Award. He is a fellow of the IACR and the ACM.

2025-02-28 Outreach to society. Female Mentoring Session
Radical Software: Women, Art & Computing 1960–1991

SPyCoDe supports the symposium organized by TU Wien Informatics, Kunsthalle Wien, and the Wolfgang Pauli Institute (WPI), which is part of an exhibition examining the history of digital art through a feminist lens. The focus is on women who used computers as both tools and subjects, and on artists whose work is inherently computational. Co-organizer Prof. Laura Kovács views the symposium as an essential platform for discussing the central themes of the exhibition, which showcases contributions from distinguished female researchers and artists. Keynote speeches and panel discussions will underscore and delve into the pivotal roles women have played in advancing computer technology and digital art. Additionally, within the Q&As, panel discussions and closing networking events, female participants will have further opportunities to interact and discuss with prominent role models in computer science, in particular with Ina Wagner (TU Wien), Nadia Thalmann (MIRALab, University of Geneva), and Gerti Kappel (TU Wien Informatics).
The full program is available here .

2025-02-26 Presentation
NDSS Symposium 2025

The Network and Distributed System Security Symposium (NDSS ) 2025, which took place in San Diego, California from February 24 to 28, showcased four impactful papers from SPyCoDe researchers. These works explored advanced topics ranging from blockchain security to innovative attack vectors.
One notable presentation, “Alba: The Dawn of Scalable Bridges for Blockchains ” by G. Scaffino, L. Aumayr, M. Bastankhah, Z. Avarikioti, and M. Maffei, introduced the Pay2Chain bridge. This innovative tool leverages off-chain solutions to enhance the efficiency of blockchain interoperability, demonstrating secure, efficient, and trustless transactions based on off-chain events.
Another critical study, “CounterSEVeillance: Performance-Counter Attacks on AMD SEV-SNP ” by S. Gast, H. Weissteiner, R.L. Schröder, and D. Gruss, revealed a novel side-channel attack that exploits performance counter data in AMD’s confidential virtual machines. This research demonstrates how sensitive data can be extracted, posing significant implications for the security of virtual environments.
Additionally, “KernelSnitch: Side-Channel Attacks on Kernel Data Structures ” by L. Maar, J. Juffinger, T. Steinbauer, D. Gruss, and S. Mangard, detailed a method for exploiting kernel data structures to extract sensitive information. This attack illustrates vulnerabilities in systems, even those without shared hardware elements.
Lastly, “Secret Spilling Drive: Leaking User Behavior through SSD Contention ” by J. Juffinger, F. Rauscher, G. La Manna, and D. Gruss, investigated how SSD contention could be used to create a covert channel that leaks user behavior. This study highlights the security risks associated with modern SSDs and their implications for user privacy.
These papers not only address current security challenges but also propose innovative solutions, demonstrating SPyCoDe’s significant contributions to the field of network and system security.

2025-02-20 Keynote
Daniel Gruss delivered the keynote ‘Every Threat Model is Wrong’ at RuhrSec 2025.

Abstract. Security is the tension between an adversary trying to break into a system and a defender trying to prevent this. This game is inherently asymmetric, as the defender tries to anticipate what the adversary could do and the adversary tries to find anything the defender overlooked. Thus, it is at the core of security that threat models are time and again invalidated. In this keynote, we’ll explore some historic examples including the change from isolated to interconnected systems, the change of the root of trust with TEEs, and lastly the change from carbon-ignorant security to carbon-aware security. Finally, we will discuss why threat models are still relevant and how they can guide security research in a constantly evolving landscape.

2025-02-19 Presentation
Jonas Juffinger presented at the 1st Microarchitecture Security Conference (uASC ‘25).

Title. An Analysis of HMB-based SSD Rowhammer
Abstract. Rowhammer has been shown to be an extensive attack vector. In the years since its discovery, numerous exploits have been shown, attacking a wide range of targets from kernels, through web browsers to machine learning models. These attacks were not always mounted from code running on the CPU of a system. Various devices peripheral to the CPU, like GPUs or network cards, can cause Rowhammer bit flips through DMA accesses to the main memory. In this work, we take a look at solid state drives (SSDs) and if they can be exploited as confused deputies to perform Rowhammer attacks. With the introduction of NVMe, a standardized protocol that allows SSDs to communicate directly over PCIe with the CPU, SSDs have reached performance numbers of a million input/output operations per second. PCIe also enables SSDs to use DMA for direct accesses to the main memory. This led to the introduction of the host memory buffer (HMB) feature, that allows SSDs to use a small fraction of the host DRAM. We are the first to reverse engineer how different SSDs utilize this host memory buffer and answer the question if the accesses from the SSD to the HMB are a potential attack vector to cause Rowhammer bit flips. Our analysis of three SSDs shows that bit flips in the HMB cause the SSDs to lock up, which results in a denial of service or, even worse, data loss. We also show how we can cause frequent accesses from the SSD to the HMB on all three SSDs. On one SSD, we reach 5,000 DRAM accesses per refresh interval. We measure the Rowhammer impact of these accesses and show that they are effectively hammering the DRAM. However, 5,000 DRAM accesses are not enough to cause Rowhammer bit flips, even on modern, highly vulnerable DRAM.

2025-02-17 Research Seminar
Network-level vulnerabilities in cryptocurrencies

2025-01-31 Outreach to society
Computer science is general education and should become a mandatory subject.

In his guest commentary for Der Standard, Prof. Roderick Bloem argues that computer science should become a mandatory subject in Austrian schools, on par with mathematics and German. He emphasizes that in the digital age, understanding core concepts of computer science—such as algorithmic thinking, abstraction, programming, and problem analysis—is essential for all citizens to navigate the modern world critically and responsibly.

Bloem highlights the limitations of current digital education, which primarily focuses on media literacy and the ethical use of technology. He argues that this should be complemented by computer science as a distinct subject. He outlines several key benefits of making computer science a mandatory subject. First, it ensures that digital literacy becomes an essential part of general education. It also improves students’ career prospects and helps address the shortage of skilled professionals. By introducing children — especially girls — to future-oriented topics, it promotes greater diversity in the field. Furthermore, it empowers society to shape digital policy independently and responsibly. Finally, computer science is engaging and directly relevant to everyday life.

Bloem also points to the lack of qualified computer science teachers in Austria and calls for action. He suggests that establishing computer science as a full subject with final exams (Matura) would motivate more students to pursue teaching degrees in informatics.

He concludes by urging the next Austrian government to take immediate steps to establish Austria as a leader in digital education.

2025-01-29 Outreach to society
Vienna Innovation Conference

Martina Lindorfer participated in the panel ‘@Risk: Are Our Data Safe?’ at the 10th Vienna Innovation Conference. The discussion explored the evolution of data security, the impact of artificial intelligence, and Vienna’s standing in the global cybersecurity landscape.

2025-01-28 Presentation
Stefano Trevisani presented at the “Algebraic Aspects in the Design and Cryptanalysis of Modern Symmetric Cryptography” workshop (ALPSY)

The presentation, ‘Flexible Modes for Arithmetization-Oriented Compression Functions: Verifiable Computation and ZK-SNARKs,’ explored the intricate relationship between hash functions and ZK-SNARKs, specifically focusing on arithmetization-oriented hash functions and compositional paradigms. It introduced two innovative families of modes, PGV-ELC and ELC-P, aimed at enhancing the flexibility and security of cryptographic systems. Stefano emphasized the security features of these modes, especially their indifferentiability, which is vital for the robustness of cryptographic schemes. He also provided a comprehensive comparison of the security aspects of these modes, supported by benchmarking results from Groth16 and Plonky2 to assess their real-world performance. Furthermore, discussions on Merkle Tree arity benchmarks illustrated the efficiency of these modes across different configurations, aligning them with strategic cryptographic design objectives.

2025-01-27 Public Lecture
Georg Fuchsbauer will give a talk on “Space-efficient blockchains“

The talk is a part of the Public Lecture Series ‘Sustainability in Computer Science’ under the auspices of Informatik Austria .

Abstract. The move from “proof of work” to “proof of stake” has arguably overcome the problem of energy waste in blockchains. However, for public verifiability, most systems require all transactions to be stored forever, by every full node. In Bitcoin this data now amounts to over 600GB, while in Ethereum it is over 1TB. We will overview two approaches to space-efficient systems. “Mimblewimble” is a protocol where spent transactions can be erased from the blockchain while maintaining verifiability. “Mina” goes further and, using a heavy-weight cryptographic concept called zk-SNARK, reduces its blockchain size to 22kB, which will never grow.

2025-01-15 Retreat
Retreat in Semmering

2024-12-20 Distinguished Lecture
Lecture by Christoph Kerschbaumer (Mozilla) “Towards a Secure and Privacy-Respecting Web“

Abstract. The Hypertext Transfer Protocol, generally displayed as http in a browsers address-bar, is the fundamental protocol through which web browsers and websites communicate. However, data transferred by the regular http protocol is unprotected and transferred in cleartext, such that attackers are able to view, steal, or even tamper with the transmitted data. Carrying http over the Transport Layer Security (TLS) protocol, generally displayed as https in the address-bar of a browser, fixes this security shortcoming by creating a secure and encrypted connection between the browser and the website.

Bio: Dr. Christoph Kerschbaumer has over two decades of experience in software engineering and computer security. His work ranges from designing secure systems with fail-safe defaults to fighting cross-site scripting to preventing man-in-the-middle attacks. Currently he is managing the Firefox Security Engineering team at Mozilla and is mentoring software engineers around the world to reach their full potential. He received his PhD in Computer Science from the University of California, Irvine, where he focused his research on information flow tracking techniques within web browsers. Prior to being a graduate research scholar, he received a M.Sc. and B.Sc. in Computer Science from the Technical University Graz, Austria.

2024-12-19 Outreach to society
KURIER-TV’s “Spontan gefragt”

Martina Lindorfer joined the recent episode of KURIER-TV’s “Spontan gefragt” as an IT security expert and computer scientist. Along with IT and business consultant Georg Krause, she discussed the complex world of cybercrime, shedding light on the sophisticated nature of modern hacking operations and explored various aspects of digital threats and defensive strategies.

2024-12-16 Research Seminar
Provable Side-Channel Resilience in Hardware and Software

2024-12-09 Research Seminar
Computationally Sound Automated Protocol Verification

2024-12-09 Recognition
Martina Lindorfer is named a Senior Fellow at the Applied Computer Security Associates (ACSA)

The prestigious recognition follows Martina’s outstanding contributions, including two years as Program Committee Chair at Annual Computer Security Applications Conference and two prior years as Artifact Evaluation Chair.

2024-11-26 Distinguished Lecture
Lecture by Adam O’Neill (University of Massachusetts, Amherst) “Idealized Models in Cryptography: What, Why, and Where to Now?“

Abstract: Provable security is the science of building cryptographic protocols out of building blocks in a sound way. Namely, one proves the only way to break a protocol is to break one of the building blocks. But does every secure protocol have such a proof? What if we can’t find one? This talk will introduce the concept of “idealized models,” which are artificial models of computation created by cryptographers to address this issue. We will describe what idealized models are and why they are used. Then, we will describe our on-going line of research aimed at better analyses in such models, as well as ultimately transitioning the proofs to do without idealized models. This gives greater assurance in the security of many widely used cryptographic protocols. The talk will be high-level and not assume previous knowledge of cryptography.

Bio: Adam O’Neill is an Assistant Professor in the Manning College of Information and Computer Sciences at the University of Massachusetts, Amherst. Previously, he was an Assistant Professor of Computer Science at Georgetown University. He received his Ph.D. in Computer Science at the Georgia Institute of Technology and held postdoctoral appointments at the University of Texas at Austin and Boston University. Recently, he received the CRYPTO 2022 Test-of-Time Award.

2024-11-25 Public Lecture
Krzysztof Pietrzak will give a talk on “Sustainable Blockchains“

The talk is a part of the Public Lecture Series ‘Sustainability in Computer Science’ under the auspices of Informatik Austria .

Abstract. The Bitcoin blockchain achieves consensus in an open setting, i.e., where everyone can participate. This was believed to be impossible, the key idea to make this possible was to use computing power rather than some kind of identities for voting through “proofs of work”. Unfortunately, this approach is not sustainable: the Bitcoin blockchain burns roughly as much electricity as a country like Austria. We will outline sustainable alternatives for achieving a Bitcoin-like blockchain, with a focus on using disk space instead of computation and how this is realized in the Chia Network blockchain.

2024-11-18 Outreach to society
FinTechWeek Vienna Opening 2024: Cybersecurity in the Age of AI

Prof. Matteo Maffei will deliver a keynote at FinTechWeek Vienna Opening 2024. As artificial intelligence continues to transform the cybersecurity landscape, it introduces both new risks and opportunities. The keynote will explore the extensive impacts of AI on cybersecurity, highlight key threats, and discuss collaborative research strategies to stay ahead in this dynamic field.

2024-11-15 Distinguished Lecture
Lecture by Ben Stock (CISPA Helmholtz Center for Information Security) “Reproducible and Ethical Web Security Measurements“

Abstract: The Web is a great place to measure many things: client-side headers, JavaScript functionality, or insecure server-side code. In this talk, I will share insights into Web measurements from two angles: first, can we make Web measurement reproducible by design such that others can confirm or refute our findings? Second, where are the red lines when considering server-side security checks such as looking for SQL injections?

Bio: Ben Stock is a tenured faculty at the CISPA Helmholtz Center for Information Security in Saarbrücken, Germany. Ben leads the Secure Web Application Group at CISPA, and his research focuses on various aspects of Web and network security, with a recent focus in particular on (un)usability of security mechanisms. His group regularly publishes at all major security conferences and Ben serves on the PC and in chair roles for various security conferences. Beyond the focus on academic output, together with his students, he regularly aims to bridge the gap between scientists and practitioners through talks at non-academic conferences like OWASP AppSec or Ruhrsec.

2024-11-08 Achievement
TUW Team Secures Third Place in CSAW Student Cybersecurity Competition

Lea Salome Brugger, a former master’s student at TU Wien and now a PhD student at ETH Zürich, won 3rd place at the CSAW Applied Research Competition in cybersecurity. She presented CheckMate , a collaborative project developed with Laura Kovács, Anja Petković Komel, Sophie Rain, and Michael Rawson. The competition was organized for the 8th time by Grenoble INP - Esisar and the LCIS laboratory, focusing on research that has a practical impact. Finalists presented their work to a jury of industrial experts.

2024-10-28 Distinguished Lecture
Lecture by Joel Reardon (University of Calgary) “Anonymity, Consent, and Other Noble Lies: An Empirical Study of the Data Economy“

Abstract: While legal scholars have cited decades of computer science research that demonstrates why anonymity is a hard problem (and that datasets should not be labelled as “anonymous” cavalierly), industry and legal practitioners have not heeded those warnings: many organizations trafficking in consumer data continue to make assertions that, for example, hashed email addresses are anonymous and cannot reveal the original email address, and that device-based identifiers, such as advertising IDs, only identify devices and not people.
We acquired datasets from multiple data brokers to empirically demonstrate why these assertions are false. Using publicly available email addresses found in data breaches posted on the Internet, we show that one can reidentify 88% of the hashed email addresses that we obtained. Reidentifying hashed email addresses need not rely on illicit data: by constructing rainbow tables, we reidentified a majority of the hashed email addresses. In all cases, the hashed email addresses were linked to other device-based identifiers (e.g., mobile data advertising IDs, IPs, etc.), demonstrating why device-based identifiers have long been considered personally identifiable information.
Relatedly, organizations trafficking in this data make another assertion, that this data was collected from consumers with their consent. To evaluate this claim, we performed a survey (n = 369), in which we emailed the reidentified individuals in our datasets to recruit them to participate in a survey. This survey asked participants about their recollections of having provided consent and whether they would prefer that the data brokers delete their data.

Bio: Joel Reardon is an associate professor at the University of Calgary who researches mobile security and privacy issues and data collection done through those devices. He has also co-founded the privacy analytics company AppCensus. He received his Bachelors and Master’s at the University of Waterloo and his Doctor of Sciences at the ETH Zurich. His research has been covered by the CBC, the BBC, the Washington Post, and the Wall Street Journal, among other places. His research has received the Emilio Aced Research and Personal Data Protection Award, the CNIL - Inria Data Protection Award, and the Caspar Bowden Award for Outstanding Research in Privacy Enhancing Technologies. He likes bicycling and snowboarding and is currently trying to improve his French.

2024-10-23 Outreach to society
Humanistic AI in Vienna. AI and Me: The Citizens’ Perspective

Prof. Laura Kovács is a participant in the panel discussion on the impacts and benefits of AI for citizens at Vienna Digital Days 2024. The discussion will focus on the application perspective, exploring the impacts and potential benefits of AI in citizens’ daily lives. Key areas of focus will include technology assessment and security. The discussion will revolve around three primary topics: the labor market and education, data security, and health, with a particular emphasis on its effects on perception and medicine.

2024-10-21 Public Lecture
Daniel Gruss give a talk on “Sustainable Security.“

The talk is a part of the Public Lecture Series “Sustainability in Computer Science“ under the auspices of Informatik Austria . This lecture series, a pioneering initiative in Austria, unites all Austrian CS departments and faculties to emphasize the vital role of sustainability in computer science. It showcases research solutions for real-world challenges and inspires progress towards a sustainable future.

Abstract. Global ICT electricity consumption is already beyond 11 percent of the worldwide electricity production and still increasing. By 2030 it may reach around 25 percent. Previous approaches to improve efficiency and performance have often sacrificed security, leading to disastrous security issues like Meltdown and Spectre. Patching just these two vulnerabilities increases power consumption on affected computers by a seemingly harmless 5 percent. By 2030, this may be more than 1 percent of the global electricity production by just a single out of thousands of patches. This development is not sustainable, and in this talk, we will discuss both the problem and potential revolutionary solutions.

2024-10-21 Presentation
Jonas Juffinger presented at the 10th edition of hardware.io Netherlands.

Looking Back at 10 Years of Rowhammer Exploits

2024-10-18 Research Visit
Breaking the Web’s Invisible Walls: Studying Emerging Client-Side Vulnerabilities at Scale

Invited talk by Soheil Khodayari (CISPA) and discussion on security of JavaScript-based web applications.

2024-10-16 Distinguished Lecture
Lecture by Giancarlo Guizzardi (University of Twente) “Semantic Models for Trustworthy Systems: A Hybrid Intelligence Augmentation Program”

Abstract: Cyber-human systems are formed by the coordinated interaction of human and computational components. In this talk, I will argue that these systems can only be designed as trustworthy systems if the interoperation between their components is meaning preserving. For that, we need to take the challenge of semantic interoperability between these components very seriously. I will discuss a notion of trustworthy semantic models and defend its essential role in addressing this challenge. Finally, I will advocate that engineering and evolving these semantic models as well as the languages in which they are produced require a hybrid intelligence augmentation program resting on a combination of techniques including formal ontology, logical representation and reasoning, crowd-sourced validation, and automated approaches to mining and learning.

Bio: Prof. Dr. Giancarlo Guizzardi is a Full Professor at the University of Twente. Before joining Twente, he was a Full Professor at the Free University of Bozen-Bolzano, in the Italian Alps, where he led the Conceptual and Cognitive Modelling Research Group (CORE). Prior to that, he co-founded and co-directed the Ontology and Conceptual Modelling Research Group (NEMO) in Brazil for 10 years. He is highly active in the fields of Formal and Applied Ontology, Conceptual Modelling, Information Systems Engineering, and Enterprise Computing/Business Informatics. His research follows a multidisciplinary approach, integrating insights from Philosophy, Logics, Linguistics, and Cognitive Science to address a variety of complex challenges in these areas. He is also a Guest Professor at Stockholm University, Sweden, where he collaborates on scientific research in the fields of Value-Based Modelling, Formal and Applied Ontology in Cyber-Social Systems, and Ethical Requirements for Information Systems.
Prof. Guizzardi has published approximately 400 papers and has taken on key leadership roles in major conferences within his fields, such as ER, FOIS, IEEE CBI, and EDOC. He has served as Program Committee Chair, General Chair, Steering Committee Member, and Keynote Speaker at prominent events including ER, BPM, CAiSE, and IEEE ICSC. Currently, he is an Associate Editor for the journals Applied Ontology, Data & Knowledge Engineering, and Enterprise Modelling and Information Systems Architectures. He also serves on the Advisory Board of the International Association for Ontologies and its Applications (IAOA). In addition to his academic work, Prof. Guizzardi has led numerous technology transfer projects in areas such as Telecommunications, Risk Management, e-Government, Digital Journalism, Complex Media Management, Distributed Software Development, and Energy, among others.

2024-10-15 Lecture
Empowering Innovation: Unlocking the Potential of Privacy-Enhancing Technologies

Lecture by Prof. Dominique Schröder (TUW).

2024-10-07 Outreach to society
Happiness is endless in research

Prof. Laura Kovács shares insights from her diverse academic journey and emphasizes the importance of overcoming challenges for young researchers in her interview with Romanian Nőileg Magazine. She highlights the value of adaptability and openness to opportunities, stressing the significance of curiosity and finding joy in one’s work. Kovács encourages early-career scientists, particularly women, to embrace the challenges of research and pursue their interests with confidence. She also underscores the need for persistence in the competitive field of IT, noting the excitement of creating something new.

2024-09-30 Research Seminar
Anthemius: Efficient & Modular Block Assembly for Concurrent Execution

2024-09-27 Distinguished Lecture
Lecture by Ruzica Piskac (Yale University) “Proofs as Polynomials”

Abstract: Zero-knowledge (ZK) protocols are well-known cryptographic primitives that allow one party to prove to another party a statement without revealing anything beyond the statement. A ZK protocol consists of two parties: a “prover” and a “verifier”. In our work, the prover holds a secret formula and its proof of validity and needs to convince the verifier about the correctness of the proof. The verifier validates the prover’s claims, by checking every step of the proof. To be able to do that without revealing any details about the formula, we use so-called commitment schemes. Commitment schemes are a fundamental part of zero-knowledge protocols as they allow a prover to commit to a value while keeping it hidden, ensuring the value cannot be altered later. A polynomial commitment scheme can be used to commit polynomials and prove the properties of the polynomials. Our work encodes proofs as polynomials and transforms this way checking the proofs steps into checking relations between polynomials. By doing these, we are able to verify the proof without revealing the formulae (and the proof itself). In this talk, we focus on proofs for formulas produced in the verification process and we explain how to encode them as polynomials. Initially, we developed a protocol for validating the unsatisfiability of Boolean formulas in privacy-preserving settings. We use the resolution calculus to produce a proof of unsatisfiability: we encoded each clause appearing in the proof as a polynomial and we reduced checking the correctness of the resolution rule to checking the divisibility of two polynomials.
A natural extension of this technique is to consider more expressive logics, such as those supported by SMT (Satisfiability Modulo Theories) solvers. To this end, we extended our initial work and developed a virtual machine for validating general unsatisfiability proofs. This virtual machine can support the majority of popular theories when proving program safety while being complete and sound. To demonstrate this, we use theories of equality and linear integer arithmetic as examples. These theories require non-trivial checking procedures and we proposed optimized arithmetizations based on multiset interpretation and polynomial encodings. Finally, we will conclude the talk by outlining how this approach benefits and empowers the verification process: we can now obtain privacy while preserving correctness.

Bio: Ruzica Piskac is a Professor of Computer Science at Yale University, where she leads the Rigorous Software Engineering (ROSE) group. Her research interests span the areas of software verification, security and applied cryptography, automated reasoning, and code synthesis. Much of her research has focused on using formal techniques to improve software reliability and trustworthiness. Piskac joined Yale’s Department of Computer Science in 2013. She was previously an Independent Research Group Leader at the Max Planck Institute for Software Systems in Germany. Her research has received a range of professional honors, including multiple Amazon Research Awards, Yale University’s Ackerman Award for Teaching and Mentoring, the Facebook Communications and Networking Award, and the Microsoft Research Award for the Software Engineering Innovation Foundation (SEIF). In 2019, Yale named Piskac the Donna L. Dubinsky Associate Professor of Computer Science. Piskac holds a Ph.D. from the Swiss Federal Institute of Technology (EPFL), where her dissertation won the Patrick Denantes Prize. Her current and recent professional activities include service as Program Chair of the 37th International Conference on Computer Aided Verification and the Steering Committee of the Formal Methods in Computer-Aided Design conference. Piskac has graduated five PhD students, four of them are currently holding a position of an assistant professor of computer science.

2024-09-27 Female Mentoring Session

During an informal talk, Prof. Ruzica Piskac, Professor of Computer Science at Yale University and leader of the Rigorous Software Engineering (ROSE) group, shared her personal journey in computer science, emphasizing the challenges she faced and how she overcame them. The discussion also explored the current state of female representation in formal methods, computer science, and software engineering. Participants asked questions and shared their own experiences. Held in a warm and relaxed atmosphere, the conversation, moderated by Laura Kovacs, provided a wonderful opportunity not only to exchange insights but also to network.

2024-09-23 Summer School

Graz Security Week 2024 will be hosted by the IAIK – the Institute of Applied Information Processing and Communication at Graz University of Technology. The cybersecurity summer school is aimed at graduate students interested in security, privacy, and correctness. The main topics of the school this year include Cryptography & Cryptographic Implementations, Side Channels Privacy, and Safe AI. The program is available and registration is now open . Join us!

2024-09-05 Achievement
Best Paper Award at the Conference on Cryptographic Hardware and Embedded Systems (CHES)

Johannes Haring, Vedad Hadžić and Roderick Bloem won the Best Paper Award at CHES 2024 with their paper “Closing the Gap: Leakage Contracts for Processors with Transitions and Glitches ”

2024-08-25 Outreach to society
Dagstuhl Seminar 24351

Daniel Gruss and Jonas Juffinger, both from TU Graz, participated in the Dagstuhl Seminar 24351 on Power, Energy, and Carbon-Aware Computing on Heterogeneous Systems (PEACHES). This seminar convened leading experts from computer science, software engineering, and environmental sustainability to address pressing issues at the intersection of technology and environmental impact. The main focus was on innovative methods for achieving carbon transparency, net-zero carbon goals in AI and machine learning, and carbon-aware computing strategies across different tech domains. The seminar also featured a hackathon led by Jonas Juffinger, which focused on CPU undervolting as a technique to reduce energy consumption by up to 20% without impacting system performance. The hackathon allowed participants to experiment with undervolting settings to understand its impact on system reliability and security, including potential security vulnerabilities like cryptographic key theft.

2024-08-16 Presentation

Stefan Gast contributed to three papers that will be presented at the 33rd Usenix Security Symposium , which is focused on the latest security and privacy developments in computer systems and networks. In the paper “Divide and Surrender: Exploiting Variable Division Instruction Timing in HQC Key Recovery Attacks” authors R. L. Schröder, S. Gast, and Q. Guo identify a critical side-channel vulnerability in the Hamming QuasiCyclic (HQC) algorithm. This vulnerability stems from the variable execution times of division instructions affected by the modulo operator. The paper introduces a technique called DIV-SMT, designed for processors with Simultaneous Multithreading (SMT), which precisely measures these timing variations to create a highly accurate Plaintext-Checking (PC) oracle. This innovative method enables rapid recovery of HQC secret keys, drastically reducing both the time and number of queries required compared to traditional methods. For successful exploitation, the attacker must be on the same physical core as the victim. The effectiveness of this approach was demonstrated on an AMD Zen2 machine.
The paper “SnailLoad: Exploiting Remote Network Latency Measurements without JavaScript” by the TU Graz research team introduces SnailLoad, a novel side-channel attack leveraging network latency to infer user activities on a computer without the need for direct access to network traffic. Unlike traditional side-channel attacks that typically require the attacker to directly monitor network traffic, such as through a person-in-the-middle (PITM) attack or by being in close proximity to WiFi signals, SnailLoad only necessitates that the victim loads assets from an attacker-controlled server. This method utilizes network latency fluctuations as a side channel to detect activities like video watching or website browsing. “The main threat here is that any TCP server can stealthily obtain latency traces from any clients connecting to it,” explained Stefan Gast to SecurityWeek . The research team has further expanded public understanding of this threat by launching a dedicated website that offers a detailed description and a live demonstration of SnailLoad, providing real-world insights into how the attack functions.
The capability of hackers to spy on individuals through any device connected to the internet has captured considerable media attention. The Independent warns that SnailLoad effectively bypasses conventional security measures such as firewalls and VPNs. “When the victim accesses a website, watches an online video, or speaks to someone via video, the latency of the internet connection fluctuates in a specific pattern that depends on the particular content being used,” Stefan Gast further detailed. Testing showed that the researchers could spy on users watching videos with a 98% success rate, with the method proving particularly effective when the internet connection was slow and the videos were of substantial size.
More media coverage about SnailLoad is available through the following links: DER STANDARD , heise online .
At the symposium, the paper titled “SLUBStick: Arbitrary Memory Writes through Practical Software Cross-Cache Attacks within the Linux Kernel” by L. Maar, S. Gast, M. Unterguggenberger, M. Oberhuber, and S. Mangard will also be presented.

2024-08-14 Distinguished Lecture
Lecture by Nikos Vasilakis (Brown University) “Security in a World of Software Supply-Chain Vulnerabilities”

Abstract: Modern software incorporates thousands of third-party components. Bugs or security vulnerabilities in these components can seriously compromise the integrity of incorporating applications. Because of their widespread use, and the difficulty of vetting the enormous number of integrated components for vulnerabilities, they comprise a compelling target for attackers, who purposefully insert vulnerabilities into widely used components with the goal of compromising the integrity of entire software ecosystems. I will present a series of systems that leverage component boundaries to offer automated solutions to vulnerabilities that appear in the software component supply chain. These solutions leverage system- and language-level containment techniques to prevent different classes of attacks from affecting these applications and the broader system in which they execute. Combined, they provide a holistic and in-depth transformation-based approach to securing software ecosystems.

Bio: Nikos Vasilakis is an Assistant Professor of Computer Science at Brown University. His research encompasses systems, programming languages, and security — and has been recognized by several distinguished paper awards. His current focus is on automatically transforming systems to add new capabilities such as parallelism, distribution, and security — against a variety of threat models. Nikos is also the chair of the Technical Steering Committee behind PaSh, a shell-script optimization system hosted by the Linux Foundation.

2024-08-06 Lecture
Laura Kovács delvers a lecture “First-Order Theorem Proving” at Marktoberdorf Summer School 2024

First-order theorem proving is one of the earliest research areas within artificial intelligence and formal methods. It is undergoing a rapid development thanks to its successful use in program analysis and verification, security analysis, symbolic computation, theorem proving in mathematics, and other related areas. Breakthrough results in all areas of theorem proving have been obtained, including improvements in theory, implementation, and the development of powerful theorem proving tools. However, recent developments are not always easily accessible to non-specialists. This mini-lecture series presents the theory and practice behind the development of powerful theorem proving tools. The workhorse used for a demonstration of concepts discussed at the tutorial will be our theorem prover Vampire. The tutorial will first focus on practicalities while using first-order Vampire for validating mathematical theorems. We will then further introduce the core concepts of automating first-order theorem proving in first-order logic with equality. We will discuss the resolution and superposition calculus, introduce the saturation principle, present various algorithms implementing redundancy elimination, and demonstrate how these concepts are implemented in Vampire.

2024-07-08 Presentation
Stefano Trevisani presented at the 37th IEEE Computer Security Foundations Symposium (CSF 2024)

Title. On Efficient and Secure Compression Functions for Arithmetization-Oriented Hashing
Abstract. ZK-SNARKs, a fundamental component of privacyoriented payment systems, identity protocols, or anonymous voting systems, are advanced cryptographic protocols for verifiable computation: modern SNARKs allow to encode the invariants of a program, expressed as an arithmetic circuit, in an appropriate constraint language from which short, zero-knowledge proofs for correct computations can be constructed. One of the most important computations that is run through SNARK systems is the verification of Merkle tree (MT) opening proofs, which relies on the evaluation of a fixed-input-length (FIL) cryptographic compression function over binary MTs. As classical, bit-oriented hash functions like SHA-2 are not compactly representable in SNARK frameworks, Arithmetization-Oriented (AO) cryptographic designs have emerged as an alternative, efficient solution. Today, the majority of AO compression functions are built from permutation-based hashing modes, such as Sponge. While this approach allows cost savings, compared to blockcipher-based modes, as it does not require key-scheduling, AO blockcipher schedulers are often cheap to compute. Furthermore, classical bitoriented cryptography has long studied how to construct provably secure compression functions from blockciphers, following the Preneel-Govaerts-Vandewalle (PGV) framework. The potential efficiency gains together with the strong provable security foundations in the classic setting, motivate the study of AO blockcipher-based compression functions. In this work, we propose AO PGV-LC and PGV-ELC, two AO blockcipher-based FIL compression modes inspired by and extending the classical PGV approach, offering flexible input and output sizes and coming with provable security guarantees in the AO setting. We prove the collision and preimage resistance in the ideal cipher model, and give bounds for collision and opening resistance over MTs of arbitrary arity. We compare experimentally the AO PGV-ELC mode over the HADES blockcipher with its popular and widely adopted Sponge instantiation, POSEIDON, and its improved variant POSEIDON2. Our resulting constructions are up to 3× faster than POSEIDONAND 2× faster than POSEIDON2 in native x86 execution, and up to 50% faster in the Groth16 SNARK framework. Finally, we study the benefits of using MTs of arity wider than two, proposing a new strategy to obtain a compact R1CS constraint system in such case. In fact, by combining an efficient parametrization of the HADES blockcipher over the PGV-ELC mode, together with an optimal choice of the MT arity, we measured an improvement of up to 9× in native MT construction time, and up to 2.5× in proof generation time, compared to POSEIDON over binary MTs.

2024-07-06 Workshop
Asynchronous Hyperproperties: from Theory to Practice

Hyperproperties are a general framework to reason about properties requiring comparing multiple system executions, like security properties or robustness requirements. In this workshop, we want to bring together practitioners from different backgrounds with theoreticians developing frameworks for specifying hyperproperties.
The workshop format will focus on discussions and promoting the interchange of ideas between different communities. Find more information at the Workshop site , CySec News .

2024-07-05 Distinguished Lecture
Lecture by Sven Bugiel (CISPA Helmholtz Center for Information Security) “Access Control in Mobile Software Stacks: Can we do fundamentally better?”

Abstract: A cornerstone of mobile privacy and security is the permission system that enables users to selectively grant or revoke apps’ access to data. This pivotal role of permissions has earned them a lot of attention over the last 15 years by the research community, who identified its shortcomings and suggested improvements to it. In this talk, we briefly recap the access control model of the permission system “under the hood” and then take a step back to question whether we can do fundamentally better at the system design level. Central to this question is the existence of an ambient authority as the root of many problems and how we can get rid of it. To give food for thought, we base this discussion on a recent research work that proposes object capabilities as alternative access control model for Android and on looking at Google Fuchsia, Google’s latest operating system that is capability-based. We present some early results that show that even Fuchsia’s design is still not a sufficient solution and what the challenges are for such a paradigm shift in access control for (mobile) software stacks.

Bio: Sven Bugiel is a security researcher focusing on (mobile) operating system security and trusted computing. In the past, he was particularly looking into mandatory access control systems for the Android OS and integrating hardware security building blocks into mobile operating systems. This interest has extended to object-capability systems and developing new confidential computing solutions. More recently, he also worked on the intersection of those topics with human-centered studies, authentication, and data science. Sven is a tenured faculty at the CISPA Helmholtz Center for Information Security in Saarbrücken, Germany since end of 2021.

2024-06-24 Distinguished Lecture
Lecture by Konrad Rieck (TU Berlin, Guest Professor at TU Wien) “On Challenges in Defending Against Code Stylometry”

Location: TU Wien, FAV Hörsaal 1 Helmut Veith (1040 Vienna, Favoritenstr. 9-11, Erdgeschoß, Room HEEG02)
Time: 16:00 – 17:00

Abstract: Source code often contains subtle stylistic patterns that can be used to identify its developer, an approach known as code stylometry. While a series of research has shown that code stylometry can recognize one programmer among hundreds of others, defenses against this approach have received little attention so far. In this talk, we address this research gap from two perspectives. First, we introduce a method for automatically imitating programming styles through semantic-preserving transformations. This method allows us to mislead correct identification and protect developers’ privacy. Second, however, we prove that true anonymity cannot be achieved in this way and that stylistic patterns remain in source code under realistic conditions. Our results thus underscore the need for raising awareness and further research into protecting developers’ privacy.

Bio: Konrad Rieck is a Professor of Computer Science at TU Berlin, where he heads the Chair of Machine Learning and Security within the Berlin Institute for the Foundations of Learning and Data. Additionally, he is a Guest Professor at TU Wien. Previously, Konrad has been working at TU Braunschweig, University of Göttingen, and Fraunhofer Institute FIRST. His research interests revolve around computer security and machine learning. His group is developing novel methods for detecting computer attacks, analyzing malicious software and discovering security vulnerabilities. Moreover, the group explores the security and privacy of learning algorithms. Konrad is also interested in efficient algorithms for analyzing structured data, such as strings, trees, and graphs. His Erdős number is 3 (Müller → Jagota → Erdős) and his Bacon number is ∞. He is a very distant academic relative of Carl Friedrich Gauß (see here), although this doesn’t help when solving math problems.

2024-06-19 Outreach to society
Chat control is a security risk for all of Europe

Matteo Maffei (TU Wien), Daniel Gruss (TU Graz), Krzysztof Pietrzak (ISTA), and René Mayrhofer (Johannes Kepler University Linz), in a dialogue with DER STANDARD, have expressed significant concerns about the proposed client-side scanning measures in the EU.

As the European Parliament reviews the child sexual abuse (CSA) prevention and combat regulation, which advocates for the preemptive scanning of messages in platforms like WhatsApp, a broad spectrum of stakeholders, including researchers, data protection organizations, and child protection centers, have raised alarm. Critics argue that this method risks compromising secure communication, exposing citizens to extensive surveillance, and potentially allowing misuse by state actors or criminals. Additionally, there is apprehension about the arbitrary classification of content as illegal, which may encroach upon freedoms such as political speech. If enforced, this policy could fundamentally alter the operation of messaging services across Europe. Encrypted services like Signal might exit the European market, while others, such as WhatsApp and Threema, could be compelled to lower their encryption standards to align with new EU regulations.

Daniel Gruss pointed out the inherent security weaknesses in client-side scanning software, noting that such systems, once deployed, are bound to harbor exploitable flaws due to their complexity. Matteo Maffei emphasized the profound impact on fundamental rights, likening the scanning process to an invasive system where every letter is read, verified, and resealed before delivery. He argued that using client-side scanning to break encryption carries huge risks that could threaten the security of all citizens.

Highlighting the importance of maintaining robust communication security, the experts advocate for more research into bolstering system security rather than diminishing it, underscoring that secure communication is a critical and well-understood pillar of IT security that must be preserved.
Find the full text of the article in German on DER STANDARD .

2024-06-11 Research Visit
Automatic On-Device Mitigation for Crypto API Misuse

Invited talk by Florian Draschbacher (TU Graz) and discussion on automatic on-device mitigation for crypto API misuse in Android applications.

2024-06-11 Achievement
Best Paper Award at HOST 2024

The paper titled “Security Aspects of Masking on FPGAs,” authored by Barbara Gigerl, Kevin Pretterhofer, and Stefan Mangard, was honored with the Best Paper Award at the IEEE International Symposium on Hardware Oriented Security and Trust (HOST) 2024.

2024-06-03 Research Visit
Formal Verification of Probe Isolating Non-Interference in Secure Circuits

TUW hosted an enriching full-day session led by SPyCoDe PIs, Laura Kovács and Roderick Bloem, focusing on the advanced topic of formal verification of probe isolating non-interference (PINI) in secure circuits. The meeting featured distinguished expert Dr. Nikolaj Bjorner from Microsoft Research, renowned for his work with the advanced SMT (Satisfiability Modulo Theories) constraint solver Z3, who contributed unique insights and expertise. Other participants included Clemens Eisenhofer and Robin Coutelier. Throughout the day, the group explored how SMT reasoning could be expanded to enhance the security features of electronic circuits, effectively increasing their resistance to various forms of interference and tampering, both with and without the use of probabilities. This event not only showcased the latest advancements in secure circuit design but also promoted collaboration among some of the brightest minds in the field. It was a day filled with stimulating exchanges, thought-provoking ideas, and meaningful knowledge sharing, setting the stage for further research.'

2024-05-21 Presentation
Simon Jeanteur presented CryptoVampire at the 45th IEEE Symposium on Security and Privacy

The presentation highlighted the results of collaborative research with Laura Kovács, Matteo Maffei, and Michael Rawson. CryptoVampire represents a significant breakthrough in protocol verification, enabling the first fully automated proofs via the innovative Computationally Complete Symbolic Attacker (CCSA) model. This advancement considerably strengthens the capabilities for automatic verification of protocols, employing a more sophisticated model than was previously possible.

2024-05-13 Research Seminar
Trapdoor Memory-Hard Functions

2024-04-29 Research Seminar
VIRAS: A Conflict-Driven Descision Procedure for mixed Integer-Real Arithmetic

2024-04-23 Distinguished Lecture
Martina Lindorfer delivered a lecture at the Cluster of Excellence CASA

Shedding Light on Data Collection and Security Issues in Modern Apps .
Abstract. Mobile phones are an integral part of every aspect of our daily lives and we use them, through a plethora of apps, for everything from communicating, to shopping and banking, to controlling the devices in our smart homes. With the goal of maximizing user experience, apps collect and process an increasing amount of private information. With the rising popularity of IoT devices, we often give up even more private information about our daily lives and habits for the sake of the convenience. This private information has become a commodity: tech monopolies and shadow brokers collect and aggregate data, not only to provide tailored content, but also for market research and targeted advertising. This process is far from transparent and our data is not always in trustworthy and secure hands. Even developers with the best intentions are faced with supply chain issues when integrating libraries, external tools, and services. While existing legislation like the GDPR, CCPA, and upcoming ones like the Cyber Resilience Act aim to protect consumers against privacy invasions and insecure products, the required techniques for automated technical analyses for their enforcement remain an open challenge. In this talk, I will present our ongoing research on developing scalable static and dynamic program analysis techniques for modern mobile and web-based apps, including their integration with IoT devices, for large-scale measurements to enable transparency and accountability in the way apps process and share private information. I will also discuss while recent privacy developments by Apple and Google seemingly increase transparency, there remains a lack of enforcement and accountability when it comes to how apps handle our data. Finally, I will touch on how new app programming paradigms break expected security and privacy guarantees.
Video

2024-04-22 Outreach to society
Prof. Martina Lindorfer was interviewed by the “Wiener Zeitung“

Prof. Martina Lindorfer and Prof. Stefan Neumann discuss Google’s 25-year dominance and its effects on competition and information accessibility in Mathias Ziegler’s article “Wie böse ist Google wirklich?“ (“How evil is Google really?“) featured in Wiener Zeitung.

2024-04-17 Distinguished Lecture
Lecture by Nikolaj Bjorner (Microsoft Research) “Formal Methods at Microsoft: Secure and Reliable Programs for Everyone, Everywhere”

Location: TU Wien, Campus Freihaus, Informatikhörsaal (1040 Vienna, Treitlstraße 3)
Time: 13:00 – 13:45

Abstract: The talk presents several research projects and tools from Microsoft Research and their impact on programming secure and reliable systems. As a common basis they take a formal methods angle where systems are viewed as mathematical objects. For the context of this talk we consider computation through lenses of calculi and measurements. We then describe how these research threads interleave with major developments from academic research and phase shifts in industry. With Microsoft rapidly pivoting on deploying and delivering AI products the talk relates the foundations with recent and current projects, including development of provably secure systems, securing smart contracts, network verification, efficient and correct compilation for ML systems, and programming systems and runtimes for interacting with AI.

Bio: Dr. Nikolaj Bjorner is a partner researcher at Microsoft Research. Nikolaj’s main line of work is around the state-of-the-art SMT constraint solver Z3. Z3 was developed with Leonardo de Mour:a, Lev Nachmanson and Christoph Wintersteiger. Z3 is used for program verification, test case generation among several applications. The work around Z3 has received several awards. Karthick Jayaraman and Nikolaj created the SecGuru tool that is used to validate firewalls and routing configurations for Microsoft Azure. In 2021 Nikolaj Bjorner was named an ACM Fellow

2024-04-17 Distinguished Lecture
Lecture by Byron Cook (UCL, TU Darmstadt, Amazon) “The Business of Proof”

Location: TU Wien, Campus Freihaus, Informatikhörsaal (1040 Vienna, Treitlstraße 3)
Time: 11:15 – 13:00

Abstract: With only a few niche exceptions, the software industry had not previously figured out how to make deep use of formal mechanical reasoning based on mathematical logic. At Amazon we have recently seen tremendous adoption of the approach by product groups, with a variety of customer-facing launches that use automated reasoning, and numerous internal proof projects. This talk describes those projects, and tries explain what went well at Amazon. The talk also describes challenges that we face to scale the approach to the next level.

Bio: Dr. Byron Cook , FREng is Professor of Computer Science at University College London (UCL). Byron is also Vice President and Distinguished Scientist at Amazon. Byron’s has worked in a variety of areas over the years, including computer/network security, program analysis/verification, programming languages, theorem proving, hardware design, operating systems, and biological systems.

2024-04-15 Research Seminar
Efficient and Secure Compression Functions for Arithmetization-Oriented Hashing

2024-04-02 Retreat
Retreat at the Institute of Science and Technology Austria

2024-04-01 Outreach to society
Why We Will Never Get Rid of Side Channels

In the April episode of the “What That Means” InTechnology Podcast, Daniel Gruss discusses with hosts Camille Morhardt and Anders Fogh (Intel) the balance between side channels and resource sharing, common challenges and how to manage them, the impact of AI on side channels, and securing critical infrastructure stored in space. Find more on YouTube .”

2024-03-26 Distinguished Lecture
Lecture by Reiner Hähnle (TU Darmstadt) “Context-aware Trace Contracts.”

Abstract: The behavior of concurrent, asynchronous procedures depends in general on the call context, because of the global protocols that govern scheduling. This context cannot be specified with the state-based Hoare-style contracts common in deductive verification. Recent work generalized state-based to trace contracts, which permit to specify internal behavior of a procedure, such as calls or state changes, but not its call context. In this talk we discuss a program logic of context-aware trace contracts for specifying global behavior of asynchronous programs. We also provide a sound proof system that addresses two challenges: First, to observe the program state not merely at the end points of a procedure, we introduce the novel concept of an observation event. Second, to combat combinatorial explosion of possible call sequences of procedures, we adapt Liskov’s principle of behavioral subtyping to the analysis of asynchronous calls.
This is a joint work with Eduard Kamburjan (U Oslo) and Marco Scaletta (TU Darmstadt).

Bio: Reiner Hähnle is Professor in Software Engineering at the Computer Science Department of TU Darmstadt. He has wide-ranging interests in the formal foundations of software design, of programming languages, and of quality assurance by verification. He is co-initiator of the KeY project that maintains the well-known, eponymous Java verification tool and he is co-designer of the active object language ABS. He is co-founder of the Tableaux and IJCAR conference series and currently SC Chair of FASE. Notably, he was the first ever Wine Chair of an international Computer Science conference at ECOOP 2014.

2024-03-18 Research Seminar
Rational protocol design

2024-03-04 Research Seminar
Comparing Apples to Androids: Discovery, Retrieval, and Matching of iOS and Android Apps for Cross-Platform Analyses

2024-02-26 Research Seminar
Secure Blockchains in Network Transition Periods

2024-02-19 Research Seminar
Secure and Verifiable Implementations of off-chains Protocols

2024-01-29 Research Seminar
Cryptanalysis Using Constraint Programming

2024-01-22 Research Seminar
Software Fault Attacks and Energy Efficiency

2024-01-15 Research Seminar
Secure implementation of the masking countermeasure on different platforms

2023-12-13 Distinguished Lecture
Lecture by Frank Leymann (Universität Stuttgart) “Post-Quantum Security.”

Abstract: We remind the underpinnings of classical encryption, factorization and elliptical curves, and their relation to discrete logarithms. After very briefly sketching the key resources of quantum computing, Shor’s algorithm is revealed to solve the discrete logarithm problem. Thus, quantum computing is jeopardizing today’s cryptographic infrastructure. Lattice-based cryptography is introduced, and a brief overview on Dilithium and Kyber is given. These two algorithms are believed to be quantum safe, i.e. they promise to resist attacks by quantum (as well as classical) algorithms. While Dilithium and Kyber are already being standardized, a broad understanding of the above security threads is missing in industry. A sketch of activities of major industry players closes the talk.

Bio: Frank Leymann is the first Kurt Gödel Visiting Professor and an honorary professor at TU Wien. He studied Mathematics, Physics, and Astronomy at the University of Bochum, Germany. After receiving his master’s degree in 1982, he pursued his PhD in Mathematics in 1984. Afterwards, he joined IBM Research and Development and worked for two decades for the IBM Software Group. In 2004, Frank Leymann was appointed as a full professor of computer science at the University of Stuttgart, where he founded the Institute of Architecture of Application Systems and serves as its director. His research interests encompass middleware in general, pattern languages, and cloud computing, with a current strong focus on quantum computing. Frank is an elected member of the Academy of Europe (Academia Europaea). He published uncountable papers in journals and proceedings, co-authored four textbooks, and holds more than 70 patents, especially in the area of workflow management and transaction processing. He served on steering-, program- and organization committees of many international conferences, and is (associated) editor of several journals. From 2006 to 2011, he was a member of the scientific directorate of Schloss Dagstuhl (Leibniz Center of Computer Science). In 2019, he was appointed as a Fellow at the Center of Integrated Quantum Science and Technology (IQST), and in 2020 he was appointed as Member of the Expert Council for Quantum Computing of the German Government.

2023-12-04 Research Seminar
Efficient Multi-tuple Leakage Detection Testing in Side-channel

2023-12-01 Research Visit
Invited talk by Michele Orrù (Sorbonne Université) “Elastic SNARKs for Diverse Environments.”

Abstract: We introduce and study elastic SNARKs, a class of proofs where the prover can select different time and memory tradeoffs, depending on the execution environment and the proved statement. The output proof is independent of the chosen configuration. We construct an elastic SNARK for rank-1 constraint satisfiability (R1CS). In a time-efficient configuration, the prover uses a linear number of cryptographic operations and a linear amount of memory. In a space-efficient configuration, the prover uses streaming algorithms and a quasilinear number of cryptographic operations with a logarithmic amount of memory. A key component of our construction is an elastic probabilistic proof. Along the way, we also formulate a streaming framework for R1CS that we deem of independent interest. We additionally contribute Gemini, a Rust implementation of our protocol. Our benchmarks show that Gemini, on a single machine, supports R1CS instances with tens of billions of constraints.

Bio: Michele Orrù is a CNRS research scientist at Sorbonne Université. Previously, he was at UC Berkeley as a research scholar. He obtained his PhD from École Normale Supérieure, and his MSc in mathematics from the University of Trento. His research focuses on building authentication mechanisms that preserve user anonymity. He works on improving the efficiency and security of zero-knowledge proofs, lightweight anonymous credential systems, and confidential transactions. In the past, Michele has contributed to Python, Debian, and Tor. He co-designed GlobaLeaks, an open-source whistleblowing platform now translated into more than 90 languages and used by more than 300 organizations. Additionally, he co-authored the cryptography behind Google’s Trust Tokens. Currently, he is actively involved in maintaining the arkworks.rs algebra crate.

2023-11-28 Presentation
SPyCoDe researchers participate in ACM CCS 2023.

Five representatives from SpyCoDe actively contributed to the ACM Conference on Computer and Communications Security (CCS) held in Copenhagen, Denmark, from November 26 to 30, 2023. This conference serves as the annual flagship event of the Special Interest Group on Security, Audit, and Control (SIGSAC) within the Association for Computing Machinery (ACM), attracting information security researchers, practitioners, developers, and users worldwide to explore cutting-edge ideas and results.

During November 27-29, the conference featured the presentation of the following research contributions:

• CheckMate: Automated Game-Theoretic Security Reasoning by Lea Salome Brugger, Laura Kovács, Anja Petković Komel, Sophie Rain, and Michael Rawson, all from TUW, in the track “Formal Methods and Programming Languages”,

• Let’s Go Eevee! A Friendly and Suitable Family of AEAD Modes for IoT-to-Cloud Secure Computation by Amit Singh Bhati (KU Leuven, Belgium), Erik Pohle (KU Leuven, Belgium), Aysajan Abidin (KU Leuven, Belgium, Elena Andreeva (TUW), Bart Preneel (KU Leuven, Belgium) in the track: “Applied Cryptography”,

• Cryptographically Enforced Memory Safety by Martin Unterguggenberger, David Schrammel, Lukas Lamster, Pascal Nasahl and Stefan Mangard, all from Graz University of Technology, in the track “Software Security”,

• IoTFlow: Inferring IoT Device Behavior at Scale through Static Mobile Companion App Analysis by David Schmidt (TUW), Carlotta Tagliaro (TUW), Kevin Borgolte (Ruhr University Bochum, Germany) and Martina Lindorfer (TUW) in the track “Network Security”.

These insightful presentations showcase SpyCoDe’s commitment to advancing knowledge and innovation in the realm of computer and communications security.

2023-11-26 Public Lecture
Martina Lindorfer joined as a speaker for the iMentor Workshop.

Individualized Cybersecurity Research Mentoring (iMentor ) Workshop co-located with the ACM Conference on Computer and Communications Security (ACM CCS) virtually. It is dedicated to attracting, mentoring, and providing career guidance to early-stage graduate students from underrepresented communities who aspire to pursue a career in computer security.

Martina gave a talk titled “IoTFlow the Making-Of: Inferring IoT Device Behavior at Scale through Static Mobile Companion App Analysis.” Using the preparation of her article presented at ACM CCS 2023 as an example, she shared with the iMentor cohort the behind-the-scenes journey of the IoTFlow paper — from its initial conception to the different iterations and revisions it underwent.

Abstract. The number of “smart” devices, that is, devices making up the Internet of Things (IoT), is steadily growing. They suffer from vulnerabilities just as other software and hardware. Automated analysis techniques can detect and address weaknesses before attackers can misuse them. Applying existing techniques or developing new approaches that are sufficiently general is challenging though. Contrary to other platforms, the IoT ecosystem features various software and hardware architectures. We introduce IoTFlow, a new static analysis approach for IoT devices that leverages their mobile companion apps to address the diversity and scalability challenges. IoTFlow combines Value Set Analysis (VSA) with more general data-flow analysis to automatically reconstruct and derive how companion apps communicate with IoT devices and remote cloud-based backends, what data they receive or send, and with whom they share it. We analyzed 9,889 manually verified companion apps with IoT-Flow to understand and characterize the current state of security and privacy in the IoT ecosystem. We discovered various IoT security and privacy issues, such as abandoned domains, hard-coded credentials, expired certificates, and sensitive personal information being shared.

2023-11-24 Achievement
Maria Eichlseder received the Hedy Lamarr Prize from the City of Vienna.

Prof. Eichlseder was honored for her contributions to the development of new methods for cryptanalysis. She is one of the designers who developed the Ascon algorithm, which earlier this year was selected by the US National Institute of Standards and Technology (NIST) as the standard for lightweight cryptography. It also won the 2019 CAESAR competition for authenticated encryption in the lightweight applications category.

Lightweight cryptography deals with cryptographic methods that are particularly suitable for use in resource-constrained environments, such as RFID tags or sensors, due to their low resource requirements. This applies in particular to the Internet of Things with its numerous small sensors and actuators, as only little energy and power are available here. Ascon is also suitable for miniature technologies such as medical implants or keyless car openers.

Hedy Lamarr Prize recognizes female researchers in Austria for their outstanding achievements in the field of information technology. The prize is named after the Vienna-born Hollywood actress and scientist Hedy Lamarr. The award winners serve as role models for the next generation and motivate young women to pursue a career in the IT industry.

2023-11-24 Research Visit
Invited talk by Christof Ferreira Torres (ETH Zurich) “Do You Trust Your Wallet? Analyzing the Privacy Risks of Web3 Wallets.”

Abstract: Blockchains are complex decentralised systems that can be divided into different layers such as peer-to-peer networking, consensus protocols, smart contracts, wallets, etc. In this talk, I will focus on the privacy aspects of Web3 wallets. With the recent hype around the Metaverse and NFTs, Web3 is getting more and more popular. The goal of Web3 is to decentralize the web via decentralized applications. Wallets play a crucial role as they act as an interface between these applications and the user. Wallets such as MetaMask are being used by millions of users nowadays. Unfortunately, Web3 is often advertised as more secure and private. However, decentralized applications as well as wallets are based on traditional technologies, which are not designed with privacy of users in mind. In this talk, we will analyze the privacy implications that Web3 technologies such as decentralized applications and wallets have on users. To this end, I will present a framework that measures exposure of wallet information. Using this framework, we studied whether information about installed wallets is being used to track users online. First, we analyzed the top 100K websites and found evidence of 1,325 websites running scripts that probe whether users have wallets installed in their browser. Second, we measured whether decentralized applications and wallets leak the user’s unique wallet address to third-parties. We intercepted the traffic of 616 decentralized applications and 100 wallets and found over 2000 leaks across 211 applications and more than 300 leaks across 13 wallets. Our study shows that Web3 poses a threat to users’ privacy and that we require new designs towards more privacy-aware wallet architectures.

Bio: Christof Ferreira Torres is a postdoctoral researcher at ETH Zurich. He is part of the Secure & Trustworthy Systems Group lead by Prof. Dr. Shweta Shinde. His research focuses on analyzing the security and privacy of distributed ledgers. He obtained a joint Ph.D. in computer science from the University of Luxembourg and the Technical University of Munich. His Ph.D. thesis focuses on the automated security assessment of smart contracts. He received the Excellent Doctoral Thesis award from the University of Luxembourg and Ripple’s Impact award for his research on the security of smart contracts. Prior to his Ph.D., he has been working as a security researcher at the Fraunhofer Institute for Applied and Integrated Security (AISEC) near Munich, Germany.

2023-11-15 Achievement
Maria Eichlseder has been awarded a prize for excellence in teaching

Maria Eichlseder, an assistant professor at IAIK, was one of the four recipients honored with a prize for excellence in teaching 2022/23 at Graz University of Technology. She received the accolade for her outstanding lecture in Cryptography.

2023-11-13 Public Lecture
Krzysztof Pietrzak gave a talk on “Sustainable Blockchains“

Tha talk is a part of the Public Lecture Series ‘Sustainability in Computer Science’ under the auspices of Informatik Austria .

Abstract. The Bitcoin blockchain achieves consensus in an open setting, i.e., where everyone can participate. This was believed to be impossible, the key idea to make this possible was to use computing power rather than some kind of identities for voting through “proofs of work”. Unfortunately, this approach is not sustainable: the Bitcoin blockchain burns roughly as much electricity as a country like Austria. We will outline sustainable alternatives for achieving a Bitcoin-like blockchain, with a focus on using disk-space instead of computation and how this is realized in the Chia Network blockchain."

2023-11-06 Research Seminar
Software-based Microarchitectural CPU Attacks

2023-11-02 Presentation
Jonas Juffinger presented “CSI:Rowhammer - Cryptographic Security and Integrity against Rowhammer“ at the Hardwear.io Security Trainings and Conference 2023 .

The research addresses Rowhammer, a severe security problem in DRAM that allows an unprivileged adversary to gain kernel privileges by inducing electrical disturbance errors. CSI:Rowhammer is a hardware-software co-designed Rowhammer mitigation with principled cryptographic security and integrity guarantees, intentionally avoiding a focus on specific Rowhammer properties. Due to its generic design, the system provides protection against all Rowhammer attacks.

The presentation delved into the comprehensive details of designing a system like CSI:Rowhammer, covering aspects such as implementing low-latency hardware correction, maximizing software correction potential, securing correction routines in software against bit flips, managing possible race conditions, ensuring compatibility with virtual machines, evaluating the entire system, and more.

Slides Video

2023-10-25 Outreach to society
Engaging school children and young people in STEM activities.

In two articles featured in the release of doIT 2/2023 in “Der Standard,” SpyCoDe members explore the significance of involving children in STEM activities and investigate the opportunities available in IT for the younger generation.

Sophie Rain introduces the “Abenteuer Informatik für Volksschule” initiative, where elementary school children visit the university to playfully delve into the world of algorithms. While programming education is now accessible to 8-year-old children, adapting content and delivery methods to align with their developmental needs and capabilities is essential. The TU Wien team is dedicated to creating an educational playground for primary and secondary school classes, fostering their interest in STEM. Sophie underscores the initiative’s crucial role in empowering girls to overcome stereotypes suggesting that technology is not for them.

Professor Maria Eichlseder shares her journey in establishing a successful career in IT. A small holiday project involving an encryption algorithm revealed to her the truly exciting nature of cryptography. Despite having limited prior knowledge in informatics from school, her fascination with cryptoanalysis led her to co-author Ascon, an authenticated encryption and hashing algorithm that has become an international standard. Today, Maria characterizes IT as an inspiring environment where individuals can initiate diverse projects, collaborate in dynamic teams, and contribute to their unique interests. The job landscape is expansive, featuring numerous companies and startups in Austria with promising earning potential. Addressing young people, she encourages them by stating, “Getting involved is fun and helps you develop personally!”

2023-10-12 Research Visit
Invited talk by Chrysoula Stathakopoulou (Chainlink Labs) “Build it Super Simple: Fast consensus on a DAG“

Abstract: After carefully breaking down the consensus problem, designing a protocol allowing high throughput and low-latency becomes easier than ever, if one finds the right abstraction that is both powerful and simple. This talk introduces BBCA (Byzantine Broadcast with Complete-Adopt), a novel broadcast primitive which builds on top of Consistent Broadcast an interactive Complete-Adopt API which allows nodes to probe its internal state. We discuss how to leverage BBCA to build high-throughput and low latency consensus on a DAG and show how this design evolves from state of the art DAG based protocols.

Bio: Chrysoula Stathakopoulou is a blockchain and distributed systems researcher at Chainlink Labs, passionate about decentralizing computation and trust with highly performant systems. Before joining Chainlink Labs, she worked at the blockchain group in IBM research focusing on consensus protocols. Her academic journey culminated in the successful completion of a PhD program at ETH Zurich.

2023-10-12 Achievement
Giulia Scaffino listed amongst Top 30 @ TU Wien Under 30.

In 2023, Giulia Scaffino (27) is listed amongst the “TUW Under 30”, a list of selected TU Wien students and employees. Similar to the” Forbes Under 30”, this list features young and extraordinary researchers and entrepreneurs from the TUW, being able to present exceptional achievements in their area of research. Giulia graduated in nuclear physics and is doing her PhD at the Security& Privacy Research Group of Matteo Maffei. She specializes on Blockchain-protocols and is currently working on a blockchain bridge called “Glimpse”, enabling cross-currency transaction between Krypto-currencies. Giulia presented her results at the renowned IT conference USENIX Security Symposium. For more details see the article featured in the current print issue of the TUW Magazine #02-2023 “Schwerpunkt: Under 30” (pages 26-28) and also her bio online .

2023-10-12 Achievement
Sophie Rain listed amongst Top 30 @ TU Wien Under 30.

Sophie Rain (28) is amongst the “TUW Under 30” in 2023, a list of selected TU Wien students and employees. Similar to the “Forbes Under 30”, this list features young and extraordinary researchers and entrepreneurs from the TUW, being able to present exceptional achievements in their area of research. Sophie is a PhD student in Laura Kovacs’ Research Unit of Formal Methods in Systems Engineering. Her work focuses on the security verification of Blockchain applications by applying mathematical concepts such as game theory, logic and most importantly automated reasoning. Her work was presented at major security conferences such as CAV 2021 and CSF 2023. Furthermore, she is leading the TU Wien initiative “Abenteuer Informatik für Volksschule”, organizing workshops for pupils. For more details see the article featured in the current print issue of the TUW Magazine #02-2023 “Schwerpunkt: Under 30” and also her bio online .

2023-10-09 Research Seminar
Information-Flow Interfaces

2023-10-09 Public Lecture
Daniel Gruss gave a talk on “Sustainable Security.“

The talk is a part of the Public Lecture Series ‘Sustainability in Computer Science’ under the auspices of Informatik Austria . This lecture series, a pioneering initiative in Austria, unites all Austrian CS departments and faculties to emphasize the vital role of sustainability in computer science. It showcases research solutions for real-world challenges and inspires progress towards a sustainable future.

Abstract. Global ICT electricity consumption is already beyond 11 percent of the worldwide electricity production and still increasing. By 2030 it may reach around 25 percent. Previous approaches to improve efficiency and performance have often sacrificed security, leading to disastrous security issues like Meltdown and Spectre. Patching just these two vulnerabilities increases power consumption on affected computers by a seemingly harmless 5 percent. By 2030, this may be more than 1 percent of the global electricity production by just a single out of thousands of patches. This development is not sustainable, and in this talk, we will discuss both the problem and potential revolutionary solutions."

Slides

2023-10-01 Outreach to society
Why Data Protection Is Important and How It Succeeds

Martina Lindorfer delivered a moderated talk , discussing the critical importance of data protection, privacy, and IT security at Vienna Humanities Festival.

2023-09-25 Research Seminar
Computationally Sound Cryptographic Protocol Automated Verification

2023-09-15 Distinguished Lecture
Lecture by Marco Mellia (Politecnico di Torino) “Data, AI and Cybersecurity - a possible cocktail?”

Abstract: Modern Artificial Intelligence technologies, led by Deep Learning, have gained unprecedented momentum over the past decade. Following this wave of “AI summer”, the network research community has also embraced AI/ML algorithms to address many problems related to network operations, management and cybersecurity. This talk will give an overview of some of the recent results in applying AI-based solution to automatically process traffic traces and detect novel attacks, prevent cybersquatting attacks, support forensic investigations, and open new opportunities to protect users from possible abuses.

Bio: Marco Mellia is a full professor at Politecnico di Torino, Italy, where he is the coordinator of the SmartData@PoliTO center on Big Data, Machine Learning and Data Science. His research interests are in the area of Internet monitoring, users’ characterisation, cyber security, and big data analytics applied to different areas. He has co-authored over 250 papers published in international journals and presented in leading conferences. He won the IRTF ANR Prize at IETF-88, and best paper award at IEEE P2P’12, ACM CoNEXT’13, IEEE ICDCS’15. He is Fellow of IEEE and Editor in Chief of the Proceedings of the ACM on Networking.

2023-09-14 Outreach to society

The TU Wien cryptography expert Prof. Elena Andreeva was featured in the Puls4 documentary Angriff aus dem Internet (Attack from the Internet).

Prof. Andreeva opens the doors to her research space and group at TU Wien, explaining the role of cryptography in today’s digital world. She also discusses how everyday devices like mobile phones can be vulnerable to cyber attacks.

The documentary sheds light on the importance of preventing cyber attacks, given their ubiquitous growth worldwide, and more specifically, in Austria. As the attackers range from criminals to state-run organizations, the targets vary from public administration and states to critical infrastructure and, not least, private individuals. The documentary presents several cyber attacks and discusses directions for prevention.

The interview with Elena Andreeva is available for reading in TU Wien Informatics News.

2023-09-11 Research Seminar
A Forkcipher-based Pseudo-Random Number Generator

2023-09-04 Summer School

Graz Security Week 2023 , organized by the Institute of Applied Information Processing and Communication (IAIK) at Graz University of Technology, is set to take place. This event is specifically tailored for graduate students who are enthusiastic about delving into the intricacies of security and correctness in computing devices. The school will cover a diverse range of topics, including Runtime Security, Side-Channels, Privacy, Secure Cryptographic Implementations, and Security Verification. It offers a unique opportunity for participants to deepen their knowledge and engage in discussions surrounding these critical aspects of computer security.

2023-07-07 Talk
Martina Lindorfer is a speaker and a mentor at EPFL School of Computer and Communication Sciences Summer Research Institute

Martina Lindorfer delivered a talk titled “Watching the Watchmen - Shedding Light on Data Collection in Mobile Apps” at The Summer Research Institute (SuRI), held at the École polytechnique fédérale de Lausanne in Switzerland.

2023-06-28 Distinguished Lecture
Lecture by Kenneth Paterson (ETH Zurich) “Cryptography in the Wild.”

Abstract: In this talk I’ll discuss a research theme that has emerged in the last few years, namely the analysis of deployed cryptographic systems. There is a small but dedicated group of researchers who do this kind of work. I’ll reflect on how we conduct this kind of research, why we do it, and what we can learn from it about how developers use (and abuse) cryptography.

Bio: Kenneth Paterson is a Professor of Computer Science at ETH Zurich, where he leads the Applied Cryptography Group and is currently the head of department. He was Program Chair for Eurocrypt 2011 and Editor-in-Chief of the Journal of Cryptology from 2017 to 2020. He co-founded the Real World Cryptography series of conferences. His research has won best paper awards at conferences including ACM CCS 2016, 2022, IEEE S&P 2022, 2023, NDSS 2012, CHES 2018, and IMC 2018. He was made a Fellow of the IACR in 2017. In 2022, he was winner of the Golden Owl best teaching award for the Department of Computer Science at ETH.

2023-06-26 Presentation
Giulia Scaffino presented “Glimpse“ at the the prestigious “USENIX Security Symposium“

Glimpse stands out as an innovative protocol, facilitating secure cross-chain token transfers in a fully decentralized manner, eliminating the need for large commercial crypto-depots. This accomplishment is the result of collaborative efforts by Giulia Scaffino, Lukas Aumayr, Zeta Avarikioti, and Matteo Maffei.

Notably, the Glimpse protocol is compatible with blockchains that have limited scripting languages. The authors provide a specific implementation of Glimpse for the Liquid Network, a Bitcoin pegged sidechain. The protocol’s security is proven within the Universal Composability (UC) framework, instilling a high level of confidence in its security guarantees. The researchers conducted an economic analysis of the Glimpse protocol, revealing that verifying a simple transaction on Bitcoin-like chains using Glimpse incurs a maximum of 700 bytes of on-chain overhead, resulting in a one-time fee of $3. This fee is only twice as much as a standard Bitcoin transaction, highlighting the cost efficiency of Glimpse. Overall, the presented advancements unlock exciting possibilities for the world of cryptocurrencies.

Slides Video

2023-06-21 Distinguished Lecture
Lecture by Christian Cachin (ETH Zurich University of Bern) “Consensus in blockchains: Overview and recent results.”

Abstract: Reaching consensus despite faulty or corrupted nodes is a central question in distributed computing; it has received renewed attention over the last years because of its importance for cryptocurrencies and blockchain networks. Modern consensus protocols in this space have relied on a number of different methods for the nodes to influence protocol decisions. Such assumptions include (1) traditional voting, where each node has one vote, (2) weighted voting, where voting power is proportional to stake in an underlying asset, and (3) proof-of-X, which demonstrates a cryptographically verifiable investment of a resource X, such as storage space, time waited, or computational work. This talk will give an overview of blockchain consensus methods and then highlight recent work on constructing new consensus protocols and analyzing existing ones.

Bio: Christian Cachin is a professor of computer science at the University of Bern, where he has been leading the Cryptology and Data Security Research Group since 2019. Prior to that he worked for IBM Research - Zurich for more than 20 years. He has held visiting positions at MIT and at EPFL and has taught at several universities during his career in industrial research. He graduated with a Ph.D. in Computer Science from ETH Zurich in 1997. He is an IACR Fellow, ACM Fellow, IEEE Fellow, recipient of multiple IBM Outstanding Technical Achievement Awards, and has also served as the President of the International Association for Cryptologic Research (IACR) from 2014-2019. With a background in cryptography, he is interested in all aspects of security in distributed systems and especially in cryptographic protocols, consistency, consensus, blockchains, and cloud-computing security. He is known for developing cryptographic protocols, particularly for achieving consensus and for executing distributed cryptographic operations over the Internet. In the area of cloud computing, he has contributed to standards in storage security and developed protocols for key management. He has co-authored a textbook on distributed computing titled Introduction to Reliable and Secure Distributed Programming. While at IBM Research he made essential contributions to the development of Hyperledger Fabric, a blockchain platform aimed at business use.

2023-06-19 Research Seminar
Verification of Game-Theoretic Security Properties for Blockchain Protocols

2023-06-14 Distinguished Lecture
Lecture by Katharina Krombholz (CISPA Helmholtz Center for Information Security) “Towards Understandable Privacy and Security Guarantees - The Human Factors Perspective.”

Abstract: Due to the digitization of everyday things, humans and their surroundings are exposed to visible and invisible computers that continuously collect and share data. As a result, it is almost impossible for users and bystanders to understand these complex data sharing models along with their implications for privacy. In this talk, I will present current trends in human-centric privacy research along with a series of lessons learned to make privacy understandable and effective for everyone.

Bio: Katharina Krombholz is a tenured faculty at the CISPA Helmholtz Center for Information Security in Saarbrücken, Germany, where she leads the usable security research group. She is PC co-chair of SOUPS 23 and 24 and active in both the security & privacy and human-computer interaction communities. Katharina Krombholz obtained her PhD from TU Wien and has been visiting researcher/faculty at various institutions around the world, including LUMS in Lahore and NII in Japan.

2023-06-05 Outreach to society
Daniel Gruss and Martina Lindorfer are the speakers at the Austrian Computer Science Day

Daniel Gruss: Security – Can we afford to have it? Can we afford not to have it?
Martina Lindorfer: Watching the Watchmen – Shedding Light on Data Collection in Mobile Apps.

2023-06-05 Research Seminar
SMT or a Shelter for Theory and Logics

2023-05-31 Distinguished Lecture
Lecture by Mooly Sagiv (Tel Aviv University) “Scaling Formal Verification to Realistic Code with Applications to DeFi Verification.”

Abstract: Deductive verification tools like Dafny and Viper compile the program into an SMT formula and then utilize SMT solvers to find potential bugs or prove their absence. These tools are used to reason about small programs. However, these techniques do not scale due to the inherent complexity of SMT solving and the need to specify exact procedure behavior. Furthermore, common coding patterns such as nonlinear expressions, unbounded data structures and indirect storage complicates SMT reasoning. We present the Certora Prover, a tool that checks the semantics of the executable code against its intended behavior written in a high-level declarative language for writing relational specifications, called CVL. Developer-written specifications in CVL have prevented billion-dollar mistakes and improved code security. The Certora Prover has secured 50% of the total value locked in the Ethereum blockchain. Also, specifications are written by Solidity developers and external security experts.

Bio: Mooly Sagiv is Full Professor, Chair of Software Systems School of Computer Science, Tel Aviv University, Israel. He is a recipient of an ERC Advanced Grant 2013. He is also the CEO of Certora, a startup company providing formal verification of smart contracts. His research focuses on easing the task of developing reliable and efficient software systems. He is particularly interested in static program analysis which combines two disciplines: automated theorem proving and abstract interpretation. In the next decade, I am hoping to develop useful techniques in order to change the ways modern software is built. I am particularly interested in proof automation, given a program and a requirement, automatically prove or disprove that all executions of the program satisfying the requirements. He is interested in developing practical solutions to proof-automation by: (i) exploring modularity of the system and (ii) relying on semi-automatic and interactive processes, where the user manually and interactively guides the proof automation, and (iii) simplifying the verification task by using domain-specific abstractions expressed in a decidable logic. He is applying these techniques to verify safety of liveness of distributed systems.

2023-05-22 Research Seminar
PYTHIA: Supercharging Parallel Smart Contract Execution with the help of Optimistic Predictions

2023-05-03 Distinguished Lecture
Lecture by Konrad Rieck (TU Berlin) “When Papers Choose their Reviewers: Adversarial Machine Learning in Conference Management Systems.”

Abstract: The number of papers submitted to scientific conferences is steadily rising in many disciplines. To handle this growth, systems for automatic paper-reviewer assignments are increasingly used during the reviewing process. These systems employ statistical topic models to characterize the papers’ content and automate their assignment to reviewers. In this talk, we investigate the security of this automation and introduce a new attack that modifies a given paper so that it selects its own reviewers. Our attack is based on a novel optimization strategy that fools the topic model with unobtrusive changes to the paper’s content. In an empirical evaluation with a (simulated) conference, our attack successfully selects and removes reviewers, while the tampered papers remain plausible and often indistinguishable from innocuous submissions.

Bio: Konrad Rieck is a professor at TU Berlin, where he leads the Chair of Machine Learning and Security as part of the Berlin Institute for the Foundations of Learning and Data. Previously, he held academic positions at TU Braunschweig, the University of Göttingen, and Fraunhofer Institute FIRST. His research focuses on the intersection of computer security and machine learning. He has published over 100 papers in this area and serves on the PCs of the top security conferences (system security circus). He has been awarded the CAST/GI Dissertation Award, a Google Faculty Award, and an ERC Consolidator Grant.

2023-04-19 Distinguished Lecture
Lecture by Alessandro Abate (University of Oxford) “Logic meets Learning - Formal Synthesis with Neural Templates.”

Abstract: I shall present recent work on CEGIS, a “counterexample-guided inductive synthesis” framework for sound synthesis tasks that are relevant for dynamical models, control problems, and software programs. The inductive synthesis framework comprises the interaction of two components, a learner and a verifier. The learner trains a neural template on finite samples. The verifier soundly validates the candidates trained by the learner, by means of calls to a SAT-modulo-theory solver. Whenever the candidate is not valid, SMT-generated counter-examples are passed to the learner for further training. I shall elucidate the ins & outs of the CEGIS framework, and display its workings on a few problems: synthesis of Lyapunov functions and of barrier certificates; hybridisation of nonlinear dynamics for safety verification; synthesis of digital controllers for continuous plants; and an application in real-time autonomy.

Bio: Alessandro Abate is Professor of Verification and Control in the Department of Computer Science at the University of Oxford, where he is also Deputy Head of Department. Earlier, he did research at Stanford University and at SRI International, and was an Assistant Professor at the Delft Center for Systems and Control, TU Delft. He received an MS/PhD from the University of Padova and UC Berkeley. His research interests lie on the formal verification and control of stochastic hybrid systems, and in their applications in cyber-physical systems, particularly involving safety criticality and energy. He blends in techniques from machine learning and AI, such as Bayesian inference, reinforcement learning, and game theory.

2023-04-18 Kick-off event

On April 18, the Technical University of Vienna (TUW) hosted the highly anticipated kick-off event of SPyCoDe, a groundbreaking research program focused on the Semantic and Cryptographic Foundations of Security and Privacy through Composite Design. Generously funded by the Austrian Science Fund (FWF), this initiative aims to delve into the complexities of security and privacy in the digital landscape. The event successfully brought together a diverse group of project participants, fostering an atmosphere of collaboration and innovation.

The presentation of the SPyCoDe program covered its purpose, methodology, research plans, 14 projects, and expected results. It captivated not only the students but also garnered approval from esteemed members of the Advisory Board, including Prof. Véronique Cortier (French National Scientific Research Center (CNRS)), Prof. Bart Preneel (Research group COSIC, KU Leuven), and Prof. Christoph Paar (Ruhr-Universität Bochum). The ensuing discussion proved fruitful, providing invaluable insights and advice crucial to the program’s success in achieving its goals.

Throughout the day, participants seized the opportunity to connect with one another, engaging in informal conversations, knowledge exchange, and thought-provoking discussions. These interactions delved into the complex topics underlying the research activities of the program. A series of cross-cutting sessions facilitated collaborative efforts between the PIs and students, fostering interdisciplinary cooperation and kick-starting joint research. These sessions focused on studying various aspects of security analysis, compositionality, reasoning, and other pertinent subjects, fostering intensive and illuminating dialogue.

The Kickoff event marked a promising beginning for the SPyCoDe research program, which aims to shed light on the intricate world of security and privacy in the digital realm. With a diverse array of projects and a dedicated team of researchers, the program is poised to make significant strides in advancing our understanding and addressing the challenges of this ever-evolving field.

2022-09-06 Start of the 1st Call for 14 PhD positions