Foundations of Cybersecurity at FaMAF

This is the webage for the course "Foundations of Cybersecurity," taking place in FaMAF from 2025-02-24 to 2025-03-07.

The course is given by Gilles Barthe (gbarthe.github.io) and Santiago Arranz Olmos (sarranz.github.io), from MPI-SP. The classes are oriented to advanced computer science students, e.g., third year and up, but open to everyone. They are of interest to PhD students, researchers, and anyone interested in developing cybersecurity tools with solid theoretical foundations.

Useful

Dates: February 24th to 28th (five classes), with three extra classes from March 5th to 7th.

Schedule: Starting at 2:00 pm. Three hours per day, one and a half hours each course, and some breaks.

Place: Lab 17, FaMAF (famaf.unc.edu.ar).

Communication: The #funcs25 channel on FaMAF's Zulip (if you are not there, contact Santiago by mail on his page).

Classes

Monday 24th: Provable Security and Spectre

Provable security, one-time pad, reductionist proofs, games, game hops, example proof of CPA security. Cut short because of power outage.

Referenced material:

An introduction to relational program verification: https://software.imdea.org/~gbarthe/__introrelver.pdf.
Spectre demo: https://github.com/crozone/SpectrePoC.
C. E. Shannon, "Communication theory of secrecy systems," in The Bell System Technical Journal, vol. 28, no. 4, pp. 656-715, Oct. 1949, doi: https://doi.org/10.1002/j.1538-7305.1949.tb00928.x.
Shafi Goldwasser and Silvio Micali. 1982. Probabilistic encryption & how to play mental poker keeping secret all partial information. In Proceedings of the fourteenth annual ACM symposium on Theory of computing (STOC '82). Association for Computing Machinery, New York, NY, USA, 365–377. https://doi.org/10.1145/800070.802212.
W. Diffie and M. Hellman, "New directions in cryptography," in IEEE Transactions on Information Theory, vol. 22, no. 6, pp. 644-654, November 1976, doi: https://doi.org/10.1109/TIT.1976.1055638.
Mihir Bellare and Phillip Rogaway. 1993. Random oracles are practical: a paradigm for designing efficient protocols. In Proceedings of the 1st ACM conference on Computer and communications security (CCS '93). Association for Computing Machinery, New York, NY, USA, 62–73. https://doi.org/10.1145/168588.168596.

Tuesday 25th: Side-Channels, Spectre, Big Picture, Semantics

Timing and cache side-channels, Spectre demo, big picture of the research line, operational semantics

Referenced material:

M. Barbosa, G. Barthe, K. Bhargavan, B. Blanchet, C. Cremers, and K. Liao, "SoK: Computer-Aided Cryptography," 2021 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, USA, 2021, pp. 777-795, doi:10.1109/SP40001.2021.00008.
CompCert: compcert.org
CakeML: cakeml.org
Formosa: formosa-crypto.org
Bernstein, D.J. Cryptographic Competitions. J Cryptol 37, 7 (2024). doi:10.1007/s00145-023-09467-1

Wednesday 26th: Constant-Time, Relational Hoare Logic

Small-step semantics with observations, definition of constant-time (CT), type system to check CT, relational properties, self-composition, product programs, Hoare logic, Relational Hoare Logic

Referenced material:

G. Barthe, P. R. D'Argenio, and T. Rezk, "Secure information flow by self-composition," Mathematical Structures in Computer Science, vol. 21, no. 6, pp. 1207–1252, 2011. doi:10.1017/S0960129511000193.
N Benton. Semantics of Program Analyses and Transformations. Lecture notes for the PAT Summer School. June 2005. https://nickbenton.name/patrevised.pdf.
An introduction to relational program verification: https://software.imdea.org/~gbarthe/__introrelver.pdf.

Thursday 27th: Type System for CT, Use cases of RHL, Non-Interference and RHL

Type systems, type system for CT, intuition of its soundness, type system for NI, relation with CT, relation with RHL

Referenced material:

John Rushby. Noninterference, Transitivity, and Channel-Control Security Policies. http://www.csl.sri.com/users/rushby/papers/csl-92-2-long.pdf.

Friday 28th: Compiler preservation of CT, Verification Condition Generation for CT

Compiler correctness, preservation of safety properties, forward and backward simulations, preservation of CT with a cube, preservation with transformers, VCGen for CT, synchronous product programs

Referenced material:

Leroy, X. A Formally Verified Compiler Back-end. J Autom Reasoning 43, 363–446 (2009). https://doi.org/10.1007/s10817-009-9155-4.
G. Barthe, B. Grégoire and V. Laporte, "Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”," 2018 IEEE 31st Computer Security Foundations Symposium (CSF), Oxford, UK, 2018, pp. 328-343, doi:10.1109/CSF.2018.00031.
Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, and Vincent Laporte. 2025. Preservation of Speculative Constant-Time by Compilation. Proc. ACM Program. Lang. 9, POPL, Article 44 (January 2025), 33 pages. https://doi.org/10.1145/3704880
Claire Jones. Probabilistic Non-determinism. http://hdl.handle.net/1842/413.

Wednesday 5th: Differential Privacy

Definition of differential privacy, applications and examples, apRHL, pRHL

Referenced material:

J. Hsu et al., "Differential Privacy: An Economic Method for Choosing Epsilon," 2014 IEEE 27th Computer Security Foundations Symposium, Vienna, Austria, 2014, pp. 398-410, doi:10.1109/CSF.2014.35.
Cynthia Dwork and Aaron Roth (2014), "The Algorithmic Foundations of Differential Privacy", Foundations and Trends® in Theoretical Computer Science: Vol. 9: No. 3–4, pp 211-407. https://dx.doi.org/10.1561/0400000042.