Student Projects

For Bachelor or Master Semester project (CS, SC, Cybersecurity)

Abstract

A proof of personhood is a mechanism to authenticate real humans online in a “one person, one vote” paradigm – preferably in a privacy-preserving fashion, without having to “identify” users.  Without careful protections, however, any proof-of-personhood mechanism might be abused through coercion, vote buying, or astroturfing, where a sufficiently-motivated and wealthy attacker simply hires, tricks, or otherwise coerces real people into serving as “minions” serving the attacker’s interests instead of their own.  A recent experience paper about the Idena proof-of-personhood project confirms this important practical risk.

One potential proof-of-personhood mechanism is based on in-person pseudonym parties, which build on the physical security principle that real humans at present still have only one body each.  While imposing a certain convenience cost, the in-person format in principle allows pseudonym parties to be combined with coercion resistance mechanisms for remote e-voting recently developed by the DEDIS lab, as a potential mitigation to the coercion and vote-buying threat.

The goal of this project is to prototype, test, and evaluate such a coercion-resistance mechanism in the context of in-person pseudonym parties.  The project will include (1) prototyping a usable mockup or barebones app (web or mobile) enabling us to carry out actual, experimental pseudonym parties with the creation of real and fake credentials for coercion resistance; (2) recruiting volunteers at or beyond EPFL to participate in an informal user study to examine the usability and perceptions of such a mechanism and related issues; (3) write a detailed report on these findings, ideally leading to a research paper publication.

Required skills: This project requires solid front-end development skills, attention to detail and particularly usability considerations, ability to communicate clearly both verbally and in writing, and a willingness to interact extensively with real people (to perform the usability study) and with relevant administrative authorities (to define and obtain review and approval of the precise plan for the usability study).

Background reading

If you would like to work on this project, please read and be familiar with the following materials:

• Can decentralized systems be truly “democratizing” – and how? (talk slides)
• E-Vote Your Conscience: Perceptions of Coercion and Vote Buying, and the Usability of Fake Credentials in Online Voting (DEDIS research paper)
• Identity and Personhood in Digital Democracy: Evaluating Inclusion, Equality, Security, and Privacy in Pseudonym Parties and Other Proofs of Personhood  (DEDIS research preprint)

Contact: [email protected]

For Master Semester project (CS, SC, Cybersecurity)

Abstract

Prof. Ford is developing a non-classical foundation for reasoning called Grounded Deduction that allows unrestricted recursive definitions, but defuses the semantic paradoxes by applying a principle called habeas quid: one must “have a thing” in order to use it.  This logic foundation appears to allow us to proceed with standard, non-paradoxical reasoning mostly as usual, with a few important caveats, while cleanly defusing many known paradoxes such as the Liar (“this sentence is false”), Curry’s (“if this sentence is true then pigs fly”), Berry’s (“The smallest positive integer not definable in under eleven words”), and Yablo’s (a countably-infinite series of numbered sentences each stating “all of the following sentences are false”).

For students with sufficient proficiency in the foundations of logic and formal reasoning, and who are highly interested and motivated, a project is available to help formalize, validate, and metalogically reason about this alternate logic foundation, using a proof assistant or automated theorem prover such as Isabelle, Coq, or Lean.  A closely-related project of interest would be to formulate and develop a grounded flavor of set theory in the context of the LISA theorem prover developed here in EPFL’s LARA laboratory.

Required skills: Strong logical, mathematical, and formal reasoning skills; curiosity about the foundations of logic, mathematics, and computer science; ideally some prior experience with formal reasoning tools such as any of those listed above; extremely strong dedication and motivation to explore an intriguing alternative universe of reasoning.

Background reading

• Reasoning Around Paradox with Grounded Deduction  (DEDIS working paper)
• Paradoxes and Contemporary Logic  (Stanford Encyclopedia of Philosophy)
• Domain theory: an introduction  (Cartwright and Parsons, Rice University)

Contact: [email protected]

For Bachelor and Master Semester project (CS, SC)

Abstract

Matchertext is a proposed cross-language syntactic discipline that enables the clean embedding of any text fragment from any conformant language into any other, while avoiding the usual need to “escape” certain characters.  MinML (pronounced like “minimal”) is an experimental markup language based on matchertext that attempts to create a more writing- and reading-friendly alternative to HTML/XML/SGML syntax that remains as powerful and general as, and cross-convertible with, these standard *ML languages.  In MinML, for example, emphasis is expressed more concisely as em[emphasis] instead of the usual <em>emphasis</em>.

There is already an experimental implementation of MinML in Go along with a patch for MinML-based Web authoring in Hugo, but there is a lot of room for further development.  For example, there are many ways in which the MinML language itself might be refined and improved; it would be nice to integrate MinML-based authoring into other popular Web and other authoring tools; and a MinML-based language for classical document authoring along the lines of LaTeX would be interesting to explore.

Required skills: Strong basic programming skills; self-motivation and interest in developing and experimentally using new languages; creativity and good taste in language design.

Background reading

• MinML: concise but general markup syntax  (blog post)
• Matchertext: an escape route from language-embedding hell?  (blog post)
• Matchertext: Towards Verbatim Interlanguage Embedding  (DEDIS working paper)

Contact: [email protected]