Privacy-preserving Automated Reasoning

Bugs in software and hardware can often to catastrophic consequences. There are various ways to improve software quality, formal verification being the most rigorous of all. In formal verification, the goal is to translate programs into formulas, and then automatically prove the correctness of these formulas. Formal methods offer a vast collection of techniques to analyze and verify these systems mathematically to ensure the correctness, robustness, and safety of software and hardware systems against a specification. Despite the significant success of formal method techniques, privacy requirements are not considered in their design.

In the last two decades, we have witnessed fascinating progress in the area of automated reasoning. Modern automated reasoning tools are now applied daily to tasks in program analysis, software engineering, hardware verification, and various other domains. The efficacy of such tools allows their application to even large-scale industrial codebases.

In this talk, we will present our work on adding a privacy-aware perspective to automated reasoning. When using automated reasoning tools, the implicit requirement is that the formula to be proved is public. We propose the concept of privacy-preserving formal reasoning. In our recent work on a zero-knowledge protocol for proving the unsatisfiability of Boolean formulas in propositional logic, we developed a highly efficient protocol for knowledge of a resolution proof of unsatisfiability. We encoded verification of the resolution proof using polynomial equivalence checking, which enabled us to use fast ZKP protocols for polynomial satisfiability.



BIO
:

Ruzica Piskac is an associate professor of computer science at Yale University. Her research interests span the areas of programming languages, software verification, automated reasoning, and code synthesis. A common thread in Ruzica’s research is improving software reliability and trustworthiness using formal techniques. Ruzica joined Yale in 2013 as an assistant professor and professor, and prior to that, she was an independent research group leader at the Max Planck Institute for Software Systems in Germany. In July 2019, she was named the Donna L. Dubinsky Associate Professor of Computer Science, one of the highest recognitions that an untenured faculty member at Yale can receive. Ruzica has received various recognitions for research and teaching, including the Patrick Denantes Prize for her PhD thesis, a CACM Research Highlight paper, an NSF CAREER award, the Facebook Communications and Networking award, the Microsoft Research Award for the Software Engineering Innovation Foundation (SEIF), the Amazon Research Award, and the 2019 Ackerman Award for Teaching and Mentoring.

Bachelor@IAIK 2022/23

We present our new open bachelor’s thesis topics and award prizes to excellent students who contributed to scientific publications this past year.

If you’re interested in joining us for your bachelor’s thesis in security, this is the best way to get an impression of our topics as well as how a bachelor’s thesis at IAIK works: You’ll hear about our research areas and current hot topics, our Bachelor@IAIK program where you can work on your thesis together with your fellow students in one of our offices if you like, and maybe you’ll get to know your supervisor while chatting along.

The event will also be the kick-off lecture in Introduction to Scientific Working (ISW) where you will be able to choose your preferred topic!   

We are looking forward to meeting you!

 

Summer School: Graz Security Week

Once again, IAIK will hold the Graz Security Week. The summer school targets graduate students interested in security and correctness aspects of computing devices. 

Click here to check out the programme, speakers, and all the details!

We are looking forward to seeing you there!

Matchmaking Encryption

Meeting ID (access code): 2733 968 8841 Meeting password: imNugMMt623

Daniele Venturi introduced a new form of encryption that we name matchmaking encryption (ME). Using ME, sender S and receiver R (each with its own attributes) can both specify policies the other party must satisfy in order for the message to be revealed. The main security guarantee is that of privacy-preserving policy matching: During decryption nothing is leaked beyond the fact that a match occurred/did not occur. ME opens up new ways of secretly communicating, and enables several new applications where both participants can specify fine-grained access policies to encrypted data. For instance, in social matchmaking, S can encrypt a file containing his/her personal details and specify a policy so that the file can be decrypted only by his/her ideal partner. On the other end, a receiver R will be able to decrypt the file only if S corresponds to his/her ideal partner defined through a policy. On the theoretical side, we define security for ME, as well as provide generic frameworks for constructing ME from functional encryption. These constructions need to face the technical challenge of simultaneously checking the policies chosen by S and R, to avoid any leakage. On the practical side, we construct an efficient identity-based scheme for equality policies, with provable security in the random oracle model under the standard BDH assumption. We implement and evaluate our scheme and provide experimental evidence that our construction is practical. We also apply identity-based ME to a concrete use case, in particular for creating an anonymous bulletin board over a Tor network.

Bachelor@IAIK 2021/22

We present our new open bachelor’s thesis topics and award prizes to excellent students who contributed to scientific publications this past year.

If you’re interested in joining us for your bachelor’s thesis in security, this is the best way to get an impression of our topics as well as how a bachelor’s thesis at IAIK works: You’ll hear about our research areas and current hot topics, our Bachelor@IAIK program where you can work on your thesis together with your fellow students in one of our offices if you like, and maybe you’ll get to know your supervisor while chatting along.

The event will also be the kick-off lecture in Introduction to Scientific Working (ISW) where you will be able to choose your preferred topic!   

We are looking forward to meeting you!

 

IAIK Christmas Special 2020

The “IAIK Christmas Special” is a yearly unique show that reviews what happened in InfoSec in 2020 and showcases recent hacks and exploits. With 300-500 viewers in a packed lecture hall, it cannot take place offline this year – now it takes place online and we will make it a better and greater show than any year before.

We invited 5 InfoSec guests, a music live act, and of course, most importantly: exciting hacks, exploits, and demos.

This special lecture is part of the TU Graz SSD and InfoSec courses.

Join on Youtube!