Usability of Verifiable E-Voting [kulyk giustolisi]
One or two sentences on the problem and prerequisites.
Projects
The Security of the the Danish railway system [carsten]
We will look at the ERMTS system, and try to verify it.
Implementation of a tally-hiding election [carsten]
Design a secure multi-party communication MPC protocol to implement a tally-hinding voting protocol.
Reverse engineering PRNGs with AI [carsten]
Modern PRNGs (pseudo random number generators) are considered secure. Use AI to see if they really are.
Checking for multiple occurrences of variable uses in programs [carsten]
A program that uses the same randomness multiple-times is often insecure, because secret information may be derived from observations and mathematical analysis. Design a checker for that.
Robust Network Intrusion Detection [bruni]
Paid thesis positions in the DIREC project on training robust network intrusion detection systems with differentiable logics. Themes are datasets, rules and training, differentiable logics, and privacy-preserving ML.
Verified Machine Learning [bruni]
Apply software verification techniques to machine learning systems, using logical specifications to guarantee intended behaviour. Can focus on tooling and foundations or on case studies such as intrusion detection and autonomous driving controllers, using the Vehicle language.
NLP for Software Verification [bruni]
Integrate LLMs with interactive theorem provers, specifically Rocq. Ideas include generating documentation, automating proofs, translating proofs between provers, and using LLMs in learning environments.
Verified Software Systems and Cryptographic Protocols [bruni]
Verify systems and protocols using Rocq and MathComp-Analysis. Targets include risk-limiting audits for voting, statistical procedures like multi-armed bandits, and security protocol verification with SSprove.
SMT/SAT Sampling for MCMC Bayesian Inference [pardo wasowski]
Combine MCMC methods with SMT/SAT solvers to explore non-zero probability regions more efficiently in models with discrete variables and hard constraints. Compare the performance against Metropolis-Hastings and hit-and-run.
Bayesian Inference for Estimating Learner Vocabulary Knowledge [pardo lungu]
Design and implement a Bayesian model for the zeeguu.org platform that estimates the probability that a learner understands a word. It uses past translations, exercises, and word frequency, and updates as the learner interacts with the platform.
Testing Thread Safety in Concurrent Programs [pardo varshosaz]
Use concurrency testing tools such as jcstress or Coyote to effectively find concurrency errors in buggy implementations of thread-safe data structures.
Thread-Safety Analysis for Data Structures with CodeQL [pardo]
Develop CodeQL queries that automatically detect data races in buggy thread-safe data structures, ideally in a language with a memory model. Done in collaboration with CodeQL at GitHub.
Unit Testing for Quantum Programs [pardo varshosaz]
Develop a unit testing method for stochastic quantum programs that determines how many executions are needed to decide with statistical guarantees whether a test passes. Implement and evaluate it in an environment such as Qiskit.
Concurrency Analysis of LLM-Generated Programs [pardo]
Use LLMs to generate thread-safe data structures and evaluate with existing analysis tools whether they contain concurrency bugs.
Privacy Risk Analysis of LLM-Generated Programs [pardo]
Use privacy risk analysis tools to determine whether programs generated by LLMs leak secret information.
Automatic Search of Privacy Parameters that Minimize Privacy Risks [pardo wasowski]
Use probabilistic programming to automatically find values for privacy parameters (epsilon in differential privacy, k-anonymity, l-diversity) that minimize privacy risks.
Exploring Bayesian Inference Methods for Quantifying Privacy Risks [pardo wasowski]
Privugger quantifies privacy risks with MCMC. Explore alternatives such as variational inference, probabilistic circuits, or symbolic exact inference, for example using Pyro.
Exact Inference Engine to Quantify Privacy Risks in Python Programs [pardo wasowski]
Build an exact inference engine for quantifying privacy risks in Python programs.
Quantitative Privacy Risk Monitoring for Data Analytics [pardo wasowski]
Design a method to monitor privacy risks dynamically in a running system rather than analysing programs statically, and evaluate it in a real language, for example with the JVM Tool Interface for Java.
Privacy Risk Analysis of Counterfactuals [pardo wasowski]
Investigate the privacy risks of counterfactual explanations for machine learning models, which may reveal information about the training data. In collaboration with Imperial College London.
Attacker Synthesis via Reinforcement Learning [pardo wasowski]
Use reinforcement learning to synthesize dangerous attackers against privacy mechanisms.
Privacy Risk Analysis with the Storm Model Checker [pardo wasowski]
Translate Python programs into models supported by the Storm model checker, such as Markov chains or Markov decision processes, and model check them to find privacy risks.
Compositional Privacy Risk Analysis [pardo]
Design a compositional method that computes the privacy risk of each module and combines the results with sound and efficient rules, instead of treating the whole system as a black box.
Re-identification Risks in Large Datasets [pardo wasowski]
Study re-identification risks in a large dataset and address the resulting scalability challenges, for instance by parallelizing the analysis.
Privacy Risk Analysis of Neural Networks with Privugger [pardo wasowski]
Use Privugger to quantify privacy risks in neural networks. This involves surveying common risk metrics, plugging networks into the analysis library, and possibly extending the tool.
Implementing Privugger in R [pardo wasowski]
Port the Privugger tool, which quantifies privacy risks in Python programs, so that it can analyze programs written in R.
Implementing a Differential Privacy Library in R [pardo wasowski]
Implement a differential privacy library in R so that statisticians and data analysts can easily use differential privacy mechanisms.
Studying the Effect of Differential Privacy on Bias [pardo wasowski]
Design experiments to evaluate how differential privacy affects bias in data, and whether it can be used where some bias must be preserved, such as in medical analysis.
Privacy Risk Analysis in MS Excel [pardo]
Apply the Privug method to quantify privacy risks in analyses performed in Excel spreadsheets.
Cyber Preparedness Advice [oksana]
Analyze existing advice on preparing for outages of telecommunication and digital services, and people's attitudes towards and experiences with it.
Impact of Cyberwarfare [oksana]
Analyze the impact of known state-actor cyberattacks on critical infrastructure, during active conflict (e.g. in Ukraine) or without it. Covers the impact on affected individuals and companies as well as cross-sectoral effects.
Digital Afterlife [oksana]
Analyze people's attitudes and practices around preparing for what happens to their digital accounts and other digital assets after their death.
OpSec on the Dark Web [oksana]
Analyze the advice, including practical experiences, that dark web users give each other for preserving their security and anonymity.
Mapping Cyber Threats in the Maritime Sector [oksana]
Research project mapping the cyber threats facing the maritime sector. Ongoing, title tentative.
Overview of Cyber Threats to Telecommunications in the Arctic [oksana]
Research project giving an overview of the cyber threats to telecommunications in the Arctic. Ongoing, title tentative.
Maintenance of AI-Generated Code in Software Projects [oksana]
Research project on how AI-generated code is maintained in software projects. Ongoing, title tentative.
Evaluating Duress Authentication Schemes in Home Security Systems [oksana]
Evaluation of duress authentication schemes in home security systems.
Non-Visual Threat Detection: Comparing Phishing Detection in Screen Reader Audio vs. Visual Text Processing [oksana]
Comparison of phishing detection when text is processed through screen reader audio versus visually.
Investigation of Hacktivist Communities and Hackers-for-Hire Groups [oksana]
Investigation of hacktivist communities and hackers-for-hire groups.
Mapping Hacking-as-a-Service on the Dark Web [oksana]
Mapping of hacking-as-a-service offerings on the dark web.
Fine-Grained Definitions and Constructions for Privacy Preserving Cryptocurrencies [bernardo]
Propose formal security definitions for cryptocurrency and smart contract systems with fine-grained privacy guarantees, along with matching constructions. The theoretical work requires knowledge of modern cryptography.
Designing Mechanisms for Accountability and KYC/AML for Privacy Preserving Cryptocurrencies [bernardo]
Design auditing mechanisms that make privacy-preserving cryptocurrencies compliant with KYC/AML regulations, including the ability to reveal a financial history when compelled by a court.
Implementing Privacy Preserving Smart Contracts Based on Multiparty Computation [bernardo]
Implement privacy-preserving smart contracts based on multiparty computation. Suitable for students at all levels with reasonable software development experience.
Designing Efficient Specific Purpose Privacy Preserving Smart Contracts for Decentralized Exchanges [bernardo]
Design efficient, special-purpose privacy-preserving smart contracts for decentralized exchanges.
Analysing and Designing Efficient Protocols for Privacy Preserving Microtransactions with State Channels [bernardo]
Analyze and design efficient protocols for privacy-preserving microtransactions using state channels.
Integrating State Channels and Privacy Preserving Smart Contracts [bernardo]
Explore how state channels can be combined with privacy-preserving smart contracts to make private contract execution more efficient.
Investigating New Alternatives to Proof-of-Work [bernardo]
Investigate alternatives to Proof-of-Work, such as Proof-of-Stake, that achieve better throughput than the few tens of transactions per second of current systems. Mostly theoretical, with modern cryptography as a prerequisite.
Investigating New Sharding Techniques [bernardo]
Investigate blockchain sharding, where parallel blockchains are maintained by separate groups of users while staying consistent with each other. This includes writing security definitions and matching protocols.
Investigating New Sidechain Techniques [bernardo]
Investigate sidechains, daughter chains that handle a specific application while staying consistent with the mother chain, including security definitions and protocols.
Better Semi-Synchronous Blockchain Consensus Protocols [bernardo]
Design better semi-synchronous blockchain consensus protocols with improved performance. Mostly theoretical, with modern cryptography as a prerequisite.
Analysing Anonymity Guarantees in Ad-Hoc Privacy Preserving Cryptocurrencies [bernardo]
Analyze open-source privacy-preserving cryptocurrencies designed without provable security to find concrete anonymity vulnerabilities, propose protocol-level fixes, and responsibly disclose them. Requires a solid programming background.
Analysing the Security of Ad-Hoc Blockchain Consensus Protocols [bernardo]
Apply vulnerability analysis techniques to open-source blockchain consensus protocols designed without provable security, propose protocol-level fixes, and responsibly disclose them.
Analysing the Security of Blockchain Applications Based on Advanced Cryptographic Protocols [bernardo]
Analyze the security of open-source blockchain applications built on advanced cryptographic protocols through code analysis and testing, then propose fixes and responsibly disclose any vulnerabilities.
Using MPC for Privacy Preserving Machine Learning [bernardo]
Use multiparty computation to perform machine learning over private data, with a focus on efficiency. Combines theory with practical implementation.
Exploring New Applications for MPC in Industry [bernardo]
Explore new applications of multiparty computation that could be useful for end-user products and industry solutions.
Circuit Garbling Schemes with Improved Efficiency for Specific Functions [bernardo]
Construct circuit garbling schemes that are more efficient for specific functions, reducing communication and local computation.
Mixing Boolean Garbled Circuits and Secret Sharing Based Arithmetic Circuits [bernardo]
Improve the integration of boolean garbled circuits with secret-sharing-based arithmetic circuits, since each is better suited to different kinds of algorithms.
Constructing Efficient Constant Rounds MPC Protocols in the Preprocessing Model [bernardo]
Construct constant-round MPC protocols in the preprocessing model, where the parties do most of the work before their inputs are known. Low round complexity matters because of internet round-trip times.
Constructing MPC with Special Verifiability Guarantees [bernardo]
Construct efficient multiparty computation protocols with special verifiability guarantees.
Exploring Fairness and Covert Security for Efficient MPC Protocols over Blockchains [bernardo]
Explore fairness and covert security for efficient MPC protocols running over blockchains.
Investigate More General and/or More Efficient Constructions of Universally Composable Oblivious Transfer [bernardo]
Investigate more general or more efficient constructions of universally composable oblivious transfer, a building block for MPC and zero-knowledge proofs. Heavy theoretical work requiring modern cryptography.
Investigate More General and/or More Efficient Constructions of Universally Composable Oblivious Transfer with Special Properties for Efficient MPC [bernardo]
Investigate universally composable oblivious transfer constructions with special properties that make MPC protocols more efficient. Heavy theoretical work.
Investigate More General and/or More Efficient Constructions of Oblivious Transfer Extension [bernardo]
Investigate more general or more efficient constructions of oblivious transfer extension. Heavy theoretical work requiring modern cryptography.
Investigate More General and/or More Efficient Constructions of Universally Composable Commitments in the Preprocessing Model [bernardo]
Investigate more general or more efficient constructions of universally composable commitments in the preprocessing model. Heavy theoretical work requiring modern cryptography.
Fine-Grained Definitions and Constructions for Privacy Preserving Cryptocurrencies [bernardo]
Propose formal security definitions for cryptocurrency and smart contract systems with fine-grained privacy guarantees, along with matching constructions. The theoretical work requires knowledge of modern cryptography.
Designing Mechanisms for Accountability and KYC/AML for Privacy Preserving Cryptocurrencies [bernardo]
Design auditing mechanisms that make privacy-preserving cryptocurrencies compliant with KYC/AML regulations, including the ability to reveal a financial history when compelled by a court.
Implementing Privacy Preserving Smart Contracts Based on Multiparty Computation [bernardo]
Implement privacy-preserving smart contracts based on multiparty computation. Suitable for students at all levels with reasonable software development experience.
Designing Efficient Specific Purpose Privacy Preserving Smart Contracts for Decentralized Exchanges [bernardo]
Design efficient, special-purpose privacy-preserving smart contracts for decentralized exchanges.
Analysing and Designing Efficient Protocols for Privacy Preserving Microtransactions with State Channels [bernardo]
Analyze and design efficient protocols for privacy-preserving microtransactions using state channels.
Integrating State Channels and Privacy Preserving Smart Contracts [bernardo]
Explore how state channels can be combined with privacy-preserving smart contracts to make private contract execution more efficient.
Investigating New Alternatives to Proof-of-Work [bernardo]
Investigate alternatives to Proof-of-Work, such as Proof-of-Stake, that achieve better throughput than the few tens of transactions per second of current systems. Mostly theoretical, with modern cryptography as a prerequisite.
Investigating New Sharding Techniques [bernardo]
Investigate blockchain sharding, where parallel blockchains are maintained by separate groups of users while staying consistent with each other. This includes writing security definitions and matching protocols.
Investigating New Sidechain Techniques [bernardo]
Investigate sidechains, daughter chains that handle a specific application while staying consistent with the mother chain, including security definitions and protocols.
Better Semi-Synchronous Blockchain Consensus Protocols [bernardo]
Design better semi-synchronous blockchain consensus protocols with improved performance. Mostly theoretical, with modern cryptography as a prerequisite.
Analysing Anonymity Guarantees in Ad-Hoc Privacy Preserving Cryptocurrencies [bernardo]
Analyze open-source privacy-preserving cryptocurrencies designed without provable security to find concrete anonymity vulnerabilities, propose protocol-level fixes, and responsibly disclose them. Requires a solid programming background.
Analysing the Security of Ad-Hoc Blockchain Consensus Protocols [bernardo]
Apply vulnerability analysis techniques to open-source blockchain consensus protocols designed without provable security, propose protocol-level fixes, and responsibly disclose them.
Analysing the Security of Blockchain Applications Based on Advanced Cryptographic Protocols [bernardo]
Analyze the security of open-source blockchain applications built on advanced cryptographic protocols through code analysis and testing, then propose fixes and responsibly disclose any vulnerabilities.
Using MPC for Privacy Preserving Machine Learning [bernardo]
Use multiparty computation to perform machine learning over private data, with a focus on efficiency. Combines theory with practical implementation.
Exploring New Applications for MPC in Industry [bernardo]
Explore new applications of multiparty computation that could be useful for end-user products and industry solutions.
Circuit Garbling Schemes with Improved Efficiency for Specific Functions [bernardo]
Construct circuit garbling schemes that are more efficient for specific functions, reducing communication and local computation.
Mixing Boolean Garbled Circuits and Secret Sharing Based Arithmetic Circuits [bernardo]
Improve the integration of boolean garbled circuits with secret-sharing-based arithmetic circuits, since each is better suited to different kinds of algorithms.
Constructing Efficient Constant Rounds MPC Protocols in the Preprocessing Model [bernardo]
Construct constant-round MPC protocols in the preprocessing model, where the parties do most of the work before their inputs are known. Low round complexity matters because of internet round-trip times.
Constructing MPC with Special Verifiability Guarantees [bernardo]
Construct efficient multiparty computation protocols with special verifiability guarantees.
Exploring Fairness and Covert Security for Efficient MPC Protocols over Blockchains [bernardo]
Explore fairness and covert security for efficient MPC protocols running over blockchains.
Investigate More General and/or More Efficient Constructions of Universally Composable Oblivious Transfer [bernardo]
Investigate more general or more efficient constructions of universally composable oblivious transfer, a building block for MPC and zero-knowledge proofs. Heavy theoretical work requiring modern cryptography.
Investigate More General and/or More Efficient Constructions of Universally Composable Oblivious Transfer with Special Properties for Efficient MPC [bernardo]
Investigate universally composable oblivious transfer constructions with special properties that make MPC protocols more efficient. Heavy theoretical work.
Investigate More General and/or More Efficient Constructions of Oblivious Transfer Extension [bernardo]
Investigate more general or more efficient constructions of oblivious transfer extension. Heavy theoretical work requiring modern cryptography.
Investigate More General and/or More Efficient Constructions of Universally Composable Commitments in the Preprocessing Model [bernardo]
Investigate more general or more efficient constructions of universally composable commitments in the preprocessing model. Heavy theoretical work requiring modern cryptography.
No projects match these filters.