Abstracts
- Speaker: Catalin Dragan
- Title: TAPESTRY: A De-centralized Service for Trusted Interaction Online
- Abstract: We present a novel de-centralised service for proving the provenance of online digital identity, exposed as an assistive tool to help non-expert users make better decisions about whom to trust online. Our service harnesses the digital personhood (DP); the longitudinal and multi-modal signals created through users' lifelong digital interactions, as a basis for evidencing the provenance of identity. We describe how users may exchange trust evidence derived from their DP, in a granular and privacy-preserving manner, with other users in order to demonstrate coherence and longevity in their behaviour online. This is enabled through a novel secure infrastructure combining hybrid on- and off-chain storage combined with deep learning for DP analytics and visualization. We show how our tools enable users to make more effective decisions on whether to trust unknown third parties online, and also to spot behavioural deviations in their own social media footprints indicative of account hijacking. This talk is based on work that appeared in IEEE Transactions on Services Computing https://ieeexplore.ieee.org/document/9089308.
- Speaker: Erman Ayday
- Title: Privacy-Preserving Genomic Data Sharing
- Abstract: With the help of rapidly developing technology, DNA sequencing is becoming less expensive. Consequently, research in genomics has gained speed in paving the way to personalized (genomic) medicine, and geneticists need large collections of human genomes to further increase this speed. Furthermore, individuals are using their genomes to learn about their (genetic) predispositions to diseases, their ancestries, and even their compatibility with potential partners. On the other hand, genomic data carries much sensitive information about its owner. By analyzing the DNA of an individual, it is now possible to learn about his disease predispositions, ancestries, and physical attributes. The threat to genomic privacy is magnified by the fact that a person's genome is correlated to his family members' genomes. The Golden State killer case is an example that such linkage can put innocent family members in shame. This talk will help bioinformaticians better understand the privacy challenges of genomic data sharing, a crucial requirement to facilitate genomic data in research and treatment. I will discuss about privacy challenges and privacy-preserving solutions when (i) an individual (data owner) shares their data with a data collector (a service provider or a public database); (ii) a data collector shares statistical information about its database; and (iii) two or more data owners or data collectors (e.g., hospitals) share their data (or databases) with each other.
- Speaker: Vincenzo Ciancia
- Title: VoxLogicA: A Spatial Model Checker (with applications in Medical
Imaging)
- Abstract: Spatial aspects of computation are prominent in Computer Science, especially when dealing with systems distributed in physical space or with image data acquired from various sources. However, formal verification techniques are usually concerned with temporal properties and do not explicitly handle spatial information.
Our work stems from the topological interpretation of modal logics, the so-called Spatial Logics. We present a topology-based approach to model checking for spatial and spatio-temporal properties. Our results include theoretical developments in the more general setting of Cech closure spaces, a study of a “collective” variant, that has been compared to region calculi in recent work, publicly available software tools, and some case studies in the setting of smart transportation.
In recent joint work with the University Hospital of Siena, we have explored the application domain of automatic contouring in Medical Imaging, introducing the tool VoxLogicA, which merges the state-of-the-art imaging library ITK with the unique combination of declarative specification and optimised execution provided by spatial model checking. The analysis of an existing benchmark of medical images for segmentation of brain tumours shows that simple VoxLogicA specifications can reach state-of-the-art accuracy, competing with best-in-class algorithms based on machine learning, with the advantage of explainability and easy replicability.
- Speaker: Thomas Haines
- Title: Verified Verifiers for Verifiable Elections
- Abstract: Verifiable electronic voting promises to secure elections even in the presence of corrupted devices, malign participants, and compromised or dishonest authorities. The theoretical study of verifiable electronic voting has made significant progress; however, the implementation of these techniques has proven to be an incredible error prone process. This talk will cover the ongoing work to reduce the gap between theory and practice by formally verifying the implementations to satisfy the required cryptographic properties.
- Speaker: Ruba Abu-Salma
- Title: Users Do Not Bite: Exploring the Adoption and Use of Encrypted Communication Tools
- Abstract: Computer security and privacy experts have always advocated the widespread adoption and use of secure communication tools. However, it remains unclear if users understand what protection these tools offer. Unlike prior work, we take a user-centered approach to evaluating the user experience, and improving the design, of secure (mainly end-to-end encrypted) communication tools.
Prior studies have shown poor usability primarily hampers the adoption of secure communication tools. However, we found – by conducting five qualitative (n=102) and two quantitative (n=425) user studies – that, in addition to poor usability, lack of utility and incorrect user mental models of secure communications are primary obstacles to adoption.
Users will not adopt a communication tool that is both usable and secure, but lacks utility (due to, e.g., the tool’s small userbase). Further, most users do not know what it means for a usable and secure tool that is widely-adopted and offers utility (e.g., WhatsApp) to be end-to-end encrypted. Incorrect mental models of encryption lead people to use less secure channels that they incorrectly perceive as more secure than end-to-end encrypted tools.
Thus, we argue the key user-related challenge for secure communications is no longer fostering adoption, but emphasizing appropriate use – by helping people who already use secure tools avoid sending sensitive information over less secure channels. By employing participatory design, we take a user-centered approach to designing effective descriptions that explain the security properties of end-to-end encrypted communications.
- Speaker: Matteo Acclavio
- Title: Logic Beyond Formulas
- Abstract: Logic and proof theory provide methods and tools used in areas such as formal verification and logic programming.
However, the formula-as-process interpretation is not as well investigated as
the formulas-as-property, formula-as-program or formula-as-type interpretations.
In fact, when we model processes as formulas, formulas are not expressive enough:
they can model some processes, e.g. those who admit a series-parallel decomposition, but not the more general cases.
To overcome this limitation and develop new proof-theoretical tools for process analysis,
in this talk I present a proof system based on unoriented graphs instead of formulas.
After proving some basic properties of the system, I show how this system can find applications in process analysis.
- Speaker: Dov Gabbay
- Title: Argumentation-based Semantics for Attack and Defense Trees
- Abstract: This paper connects between the areas and communities of Abstract Argumentation and the Attack and Defense Trees in the area of Security.
Both areas deal with attacks and defense/support and both areas rely on human applications dealing with human aggressive activities.
Our idea is to examine the different points of view of these two communities and come up with new unifying ideas
which can solve existing problems in each area.
- Speaker: James Wright
- Title: On the Use of Queuing Networks to Test the Robustness of Security Protocols
- Abstract: James will be presenting an overview of a probabilistic formal method that he has been developing over the past four years,
based on M/M/c/K queuing networks. The method was developed to fill a gap in assurances
that can be given by symbolic methods about the security of a protocol
when it comes to attacks against robustness. The methodology looks at whether a protocol can guarantee
the availability and synchronisation of state between devices.
James will explain why attacks against robustness require the development of a new class of adversary models
that is distinct from the Dolev-Yao model to be able generate nuanced attacks against robustness,
and how he encapsulated them in his methodology.
He will finally present some of the attacks that he has discovered using his methodology in the IEC61850 substation automation standard.
- Speaker: Georges-Axel Jaloyan
- Title: The ABC of Next-Gen Shellcoding
- Abstract: Shellcodes are short executable stubs that are used in various attack scenarios, whenever code execution is possible. After briefly recalling how they work in general and what interesting things they can do, besides obviously running a reverse-shell, we'll have to deal with the reality that shellcodes are usually not particularly stealthy, due in part to the very suspicious presence of non-printable characters. In a tutorial-like fashion, we'll address increasingly more complex constraints starting from basic alphanumeric shellcodes on x86, up to English looking-text shellcodes, straying into unconventional architectures like ARMv8 or even the new and trendy RISC-V.
- Speaker: Sofía Celi
- Title: The state of secure messaging: the case of OTRv4
- Abstract: OTRv4 is the newest version of the Off-The-Record messaging protocol. As
a Privacy Enhancing Technology and cryptographic work, it is a protocol
where the newest academic research intertwines with real-world
implementations, which can take different forms. This new version asks
us to revisit definitions around deniability (participation, message,
online and offline); forward and post-compromise secrecy; how to best
implement a protocol; and how important security and privacy properties
are to the world.
In this talk, we will examine the key security properties that secure
messaging protocols and applications should have and provide; how they
are implemented; and what challenges lies ahead for the secure messaging
sphere. We will explore how these properties are achieved in OTRv4, in
particular, and why they are needed in today’s world.
- Speaker: Mohamed Bourennane
- Title: Quantum Secure Communication
- Abstract: The banking, financial, and defence sectors crucially depend on communication through channels that cannot be intercepted by unauthorized people. Today, different types of sensitive information are sent within and between companies. All of these users employ cryptography to keep their data secret. Today’s cryptographic protocols rely on RSA or so-called elliptical curves methods. Unfortunately, there is no guarantee that these methods will remain safe in the near future, especially having in mind the potential growth of the computation power. Fortunately, quantum mechanics makes it possible to solve the key transfer problem in a new and proven safe manner. Unlike RSA and similar methods, it is nature’s laws that guarantee the security of quantum cryptography. In this talk, I will introduce and review our research in quantum secure communication and also the worldwide effort in quantum technologies.
- Speaker: Cheng-Te Li
- Title: Learning Sleep Quality from Daily Logs
- Abstract: Precision psychiatry is a new research field that uses advanced data mining over a wide range of neural,
behavioral, psychological, and physiological data sources for classification of mental health conditions.
In this talk, I will present a computational framework for predicting sleep efficiency of insomnia sufferers.
We predict sleep efficiency of individual users with a proposed interpretable LSTM-Attention (LA Block) neural network model.
We also propose a model, Pairwise Learning-based Ranking Generation (PLRG), to rank users with high insomnia potential in the next day.
Our computational framework can be used for other applications that analyze and handle noisy and
incomplete time-series human activity data in the domain of precision psychiatry.
Back to SRM presentations.
Contact
For questions and comments contact
Jun or
Peter
.
