The Formal Computer Science Laboratory (LIF) at Université du Québec à Chicoutimi is seeking an outstanding PhD candidate to fill a 3-year funded position on anomaly detection in an identity query management system.
- Starting date: September 1st, 2024
An identity query is any request for personal information made by an entity about an individual. These queries can take various forms and have a varying level of precision; for instance, asking if a person resides in Canada and asking for a person’s exact address are two identity queries, one of which is more precise than the other.
The project considers a system that manages the secure exchange of identity queries between a large number of individuals and organizations, and in which all queries are logged in a decentralized blockchain-type medium. The objective is to detect possible anomalies, policy violations or suspicious behavior of certain agents by analyzing identity query logs produced in real time. The project includes both a formal component, in which identity queries and their properties will be modeled using two modal logics, namely linear temporal logic and epistemic modal logic. It also has a practical aspect, where the formally defined properties will be verified in real time by the implementation of a monitor integrated into the platform of a commercial product in production in a large company.
Domaine(s) de recherche
- Privacy protection
- Runtime monitoring
- Testing and verification
Université du Québec à Chicoutimi (UQAC) is part of the largest university network in Canada. It is located in the French speaking Saguenay–Lac-Saint-Jean area, reputed for the beauty of its fjord and the majesty of its natural surroundings. UQAC welcomes 6,500 students every year, more than 1,000 of which coming from 50 different countries. The research program in Computer Science is particularly dynamic; it is the host of two Canada Research Chairs, currently includes around 20 professors and associate professors, 30 PhD and post-doctoral fellows, and more than 100 master’s students.
The doctoral work will be conducted at the Formal Computer Science Lab (https://liflab.ca), under the supervision of Pr. Sylvain Hallé, Canada Research Chair on Software Testing, Specification and Verification. LIF specializes in the application of formal methods to the testing and verification of various software systems. Past projects by faculty members of LIF have been realized in collaboration with numerous companies, including Ericsson, Industrial Alliance, Ubisoft LaForge, Devicom, and Eckinox Média.
Research at LIF is internationally recognized, and contributes to the development of concrete, high-quality software tools grounded in solid mathematical foundations. Notable long-running projects developed at LIF include the BeepBeep 3 event stream processing engine , the Artichoke blockchain monitoring system , and the Petit Poucet data lineage library . All of these initiatives have been given awards and published in top-tier international conferences over the past decade.
A very good Diploma or Master university degree in computer science, informatics, business informatics, mathematics, or a related discipline is expected. We further seek the following qualifications:
- Very good formal knowledge: theoretical computer science, mathematical logic. A background in mathematics is considered a plus.
- Good programming skills; knowledge of Java is considered a plus.
- Knowledge in blockchain technology or cryptography is a plus.
- Very good scientific communication and writing skills.
- Very good knowledge in English communication and writing.
- In-depth interest in scientific problems and the motivation for independent and goal-oriented research.
Funding of this position is ensured by grants from the Canada Research Chair on Software Specification, Testing and Verification and the Natural Science and Engineering Research Council of Canada. The candidate will receive a scholarship of a net amount of 27,000 CAD per year for three years.
Prospective applicants are asked to fill the form at https://zfrmz.com/BGLMrz4QFYzkIOZxVtpD?zf_lang=en, make sure to specify project LIF24-D3, and provide the following documents:
- Letter of motivation
- Curriculum vitae, including a) list of publications if any; b) names and contact information of at least two references
- Transcripts of undergraduate and graduate studies
- A copy of the Master’s thesis, if it has been submitted
Université du Québec à Chicoutimi is committed to equity, diversity and inclusion at all steps of its students’ curriculum; candidates from under-represented groups are especially encouraged to apply. Applications will be evaluated by a panel of three UQAC faculty members by focusing on the criteria mentioned above. Shortlisted applications will be called for an online interview to further assess their technical and communication skills.
- A. Bédard, S. Hallé. (2021). Model Checking of Stream Processing Pipelines. In Proc. TIME, 5:1-5:17. DOI 10.4230/LIPIcs.TIME.2021.5
- S. Hallé. (2018). Event Stream Processing with BeepBeep 3: Log Crunching and Analysis Made Easy. Presses de l’Université du Québec, ISBN 978-2-7605-5101-5
- S. Hallé, R. Khoury, A. El-Hokayem, Y. Falcone. (2016). Decentralized Enforcement of Artifact Lifecycles. In Proc. EDOC, 1-10. DOI 10.1109/EDOC.2016.7579380
- S. Hallé, H. Tremblay. (2021). Foundations of Fine-Grained Explainability. In Proc. CAV, Springer LNCS 12760, 500-523. DOI 10.1007/978-3-030-81688-9_24