Many formal security criteria in fields like secure compilation (e.g. full abstraction and robust hyperproperty preservation), cryptography (e.g. security games, reduction proofs, and universal composability), and information flow control share a fundamental underlying structure. This underlying structure and related concepts also appear in broader contexts like denotational semantics and computational expressiveness, yet their connections are often overlooked. This paper identifies and systematizes this structure through robust properties (criteria holding in any context), robust abstractions (ensuring preservation of robust properties from abstract to concrete systems) and the new notion of non-degrading abstractions, which guarantees that the concrete system only exhibits concrete violations that are also present in the corresponding abstract system, thereby ensuring no new violations are introduced by the abstraction. By unifying concepts from different areas into a common framework, we highlight existing but underexplored connections, provide new insights and general results, and introduce a valuable perspective for understanding and advancing formal security.
AbadiM. Protection in programming-language translations. In: Secure internet programming, Lecture Notes in Computer Science, Vol. 1603, 1999, pp.19–34. Berlin, Heidelberg: Springer Berlin Heidelberg. ISBN 9783540661306.
4.
AbateCBlancoRGargD, et al.Journey beyond full abstraction: Exploring robust property preservation for secure compilation. In: 2019 IEEE 32nd computer security foundations symposium (CSF), 2019, pp.256–25615. DOI: 10.1109/CSF.2019.00025.
5.
PatrignaniMAhmedAClarkeD. Formal approaches to secure compilation: A survey of fully abstract compilation and related work. ACM Comput Surv2019; 51(6): 1–36. DOI: 10.1145/3280984
6.
KupfermanOVardiMY. Robust Satisfaction. In: Baeten JCM and Mauw S (eds) CONCUR’99 concurrency theory, 1999, pp.383–398. Berlin, Heidelberg: Springer Berlin Heidelberg. ISBN 978-3-540-48320-5.
7.
StreicherT. Domain-Theoretic Foundations of Functional Programming. USA: World Scientific Publishing Co., Inc, 2006.
8.
BellareMDesaiAJokipiiE, et al.A concrete security treatment of symmetric encryption. In: Proceedings 38th annual symposium on foundations of computer science, 1997, pp.394–403. DOI: 10.1109/SFCS.1997.646128.
9.
LindellY. How to Simulate It – A Tutorial on the Simulation Proof Technique. Cham: Springer International Publishing, 2017.
CecchettiEMyersACArdenO. Nonmalleable information flow control. In: Proceedings of the 2017 ACM SIGSAC conference on computer and communications security, CCS ’17, 2017, pp.1875–1891. New York, NY, USA: Association for Computing Machinery. ISBN 9781450349468. DOI: 10.1145/3133956.3134054.
12.
SipserM. Introduction to the theory of computation. London: International Thomson Publishing Ltd, 1997.
13.
GordonADJeffreyA. Authenticity by typing for security protocols. J Comput Secur2003; 11: 451–519.
14.
BellareMRogawayP. The exact security of digital signatures-how to sign with rsa and rabin. In: Maurer U (ed) Advances in cryptology—EUROCRYPT ’96, 1996, pp.399–416. Berlin, Heidelberg: Springer Berlin Heidelberg. ISBN 978-3-540-68339-1.
15.
GoldwasserSMicaliSRivestRL. A digital signature scheme secure against adaptive chosen-message attacks. SIAM J Comput1988; 17: 281–308.
16.
BlumMMicaliS. How to generate cryptographically strong sequences of pseudo random bits. In: 23rd Annual symposium on foundations of computer science (sfcs 1982), 1982, pp.112–117. DOI: 10.1109/SFCS.1982.72.
17.
BlumMGoldwasserS. An Efficient Probabilistic Public-Key Encryption Scheme Which Hides All Partial Information. In: Blakley GR and Chaum D (eds) Advances in cryptology, 1985, pp.289–299. Berlin, Heidelberg: Springer Berlin Heidelberg. ISBN 978-3-540-39568-3.
GoldreichOMicaliSWigdersonA. Proofs that yield nothing but their validity or all languages in np have zero-knowledge proof systems. J ACM1991; 38: 690–728.
20.
MicaliSRogawayP. Secure computation. In: Feigenbaum J (ed) Advances in cryptology—CRYPTO ’91, 1992, pp.392–404. Berlin, Heidelberg: Springer Berlin Heidelberg. ISBN 978-3-540-46766-3.
GoguenJAMeseguerJ. Security policies and security models. In: 1982 IEEE symposium on security and privacy, 1982, pp.11–11. DOI: 10.1109/SP.1982.10014.
23.
AbadiMBanerjeeAHeintzeN, et al.A core calculus of dependency. In: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’99, 1999, pp.147–160. New York, NY, USA: Association for Computing Machinery. ISBN 1581130953. DOI: 10.1145/292540.292555.
24.
McLeanJ. Proving noninterference and functional correctness using traces. J Comput Secur1992; 1: 37–57.
ZdancewicSZhengLNystromN, et al.Secure program partitioning. ACM Trans Comput Syst2002; 20: 283–328.
27.
BlanchetB. From Secrecy to Authenticity in Security Protocols. In: Hermenegildo M and Puebla G (eds) 9th International static analysis symposium (SAS’02), Lecture Notes in Computer Science, Vol. 2477, 2002, pp.342–359. Madrid, Spain: Springer.
28.
SwaseyDGargDDreyerD. Robust and Compositional Verification of Object Capability Patterns. In: OOPSLA, 2017. ACM.
29.
BackesMHriţcuCMaffeiM. Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations. J Comput Sec2014; 22: 301–353.
30.
BengtsonJBhargavanKFournetC, et al.Refinement types for secure implementations. ACM Trans Program Lang Syst2011; 33: 8:1–8:45.
31.
BhargavanKFournetCGordonAD. Modular verification of security protocol code by typing. ACM SIGPLAN Notices2010; 45: 445–456.
32.
FournetCGordonAMaffeisS. A Type Discipline for Authorization in Distributed Systems. In: 20th IEEE computer security foundations symposium (CSF’07), 2007, pp.31–48. DOI: 10.1109/CSF.2007.7.
33.
WooTLamS. A semantic model for authentication protocols. In: Proceedings 1993 IEEE computer society symposium on research in security and privacy, 1993, pp.178–194. DOI: 10.1109/RISP.1993.287633.
34.
AbadiMGordonAD. A calculus for cryptographic protocols: the SPI calculus. Inform Comput1999; 148: 1–70.
35.
DevrieseDPatrignaniMPiessensF. Fully-abstract compilation by approximate back-translation. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’16, 2016, pp.164–177. New York, NY, USA: Association for Computing Machinery. ISBN 9781450335492. DOI: 10.1145/2837614.2837618.
36.
PlotkinG. LCF considered as a programming language. Theor Comput Sci1977; 5: 223–255.
37.
AbadiMPlotkinGD. On protection by layout randomization. ACM Trans Inf Syst Secur2012; 15(2): 1–29. DOI: 10.1145/2240276.2240279.
38.
AhmedABlumeM. Typed Closure Conversion Preserves Observational Equivalence. In: International conference on functional programming, 2008, pp.157–168. ACM. DOI: 10.1145/1411204.1411227.
39.
AhmedABlumeM. An Equivalence-Preserving CPS Translation via Multi-Language Semantics. In: International conference on functional programming, 2011a, pp.431–444. ACM. DOI: 10.1145/2034773.2034830.
40.
AbadiMRogawayP. Reconciling two views of cryptography (the computational soundness of formal encryption)*. J Cryptol2002; 15: 103–127.
41.
DevrieseDPatrignaniMPiessensF. Two parametricities versus three universal types. ACM Trans Program Lang Syst2022; 44: 23:1–23:43.
42.
AbateCAzevedo de AmorimABlancoR, et al.When good components go bad: Formally secure compilation despite dynamic compromise. In: Proceedings of the 2018 ACM SIGSAC conference on computer and communications security, CCS ’18, 2018, pp.1351–1368. New York, NY, USA: Association for Computing Machinery. ISBN 9781450356930.
43.
AgtenPStrackxRJacobsB, et al.Secure Compilation to Modern Processors. In: 2012 IEEE 25th computer security foundations symposium, 2012, pp.171–185. DOI: 10.1109/CSF.2012.12.
PatrignaniMGuarnieriM. Exorcising spectres with secure compilers. In: Proceedings of the 2021 ACM SIGSAC conference on computer and communications security, CCS ’21, 2021, pp.445–461. New York, NY, USA: Association for Computing Machinery. ISBN 9781450384544. DOI: 10.1145/3460120.3484534.
46.
Van StrydonckTPiessensFDevrieseD. Linear capabilities for fully abstract compilation of separation-logic-verified code. Proc ACM Program Lang2019; 3(ICFP): 1–29.
47.
LanckrietEBusiMDevrieseD. : A for verifying protocols that use remote attestation. In: 2023 IEEE 36th computer security foundations symposium (CSF), 2023, pp.537–551. Los Alamitos, CA, USA: IEEE Computer Society. DOI: 10.1109/CSF57540.2023.00019.
48.
TimanyAStefanescoLKrogh-JespersenM, et al.A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. Proc ACM Program Languag2017; 2: 64:1–64:28.
49.
HillerströmDLindleySLongleyJ. Effects for efficiency: asymptotic speedup with first-class control. Proc ACM Program Languag2020; 4: 100:1–100:29.
50.
PatrignaniMClarkeD. Fully abstract trace semantics for low-level isolation mechanisms. In: Proceedings of the 29th Annual ACM symposium on applied computing, SAC ’14, 2014, pp.1562–1569. New York, NY, USA: Association for Computing Machinery. ISBN 9781450324694. DOI: 10.1145/2554850.2554865.
51.
PatrignaniMClarkeDPiessensF. Secure compilation of object-oriented components to protected module architectures. Shan, Chung-chieh (ed.), 2013. Springer International Publishing; Switzerland. ISBN 9783319035413.
52.
AhmedABlumeM. An equivalence-preserving CPS translation via multi-language semantics. SIGPLAN Not2011b; 46: 431–444.
53.
BarakBGoldreichOImpagliazzoR, et al.On the (im)possibility of obfuscating programs. J ACM2012; 59(2): 1–48. DOI: 10.1145/2160158.2160159.
54.
JacobsKTimanyADevrieseD. Fully abstract from static to gradual. Proc ACM Program Lang2021; 5(POPL): 1–30. DOI: 10.1145/3434288.
55.
AbateCBlancoRCiobâcăc, et al.Trace-Relating Compiler Correctness and Secure Compilation. In: Müller P (ed.) Programming languages and systems, 2020, pp.1–28. Cham: Springer International Publishing. ISBN 978-3-030-44914-8.
56.
CanettiR. Universally composable security: a new paradigm for cryptographic protocols. In: Proceedings 42nd IEEE Symposium on foundations of computer science, 2001, pp.136–145. DOI: 10.1109/SFCS.2001.959888.
57.
BrzuskaCDelignat-LavaudAFournetC, et al.State separation for code-based game-playing proofs. In: Peyrin T and Galbraith S (eds) Advances in cryptology – ASIACRYPT 2018, 2018, pp.222–249. Cham: Springer International Publishing. ISBN 978-3-030-03332-3.
58.
CamenischJKrennSKüstersR, et al.iUC: Flexible Universal Composability Made Simple. In: Galbraith SD and Moriai S (eds) Advances in cryptology – ASIACRYPT 2019, 2019, pp.191–221. Cham: Springer International Publishing. ISBN 978-3-030-34618-8.
59.
CanettiRStoughtonAVariaM. Easyuc: Using easycrypt to mechanize proofs of universally composable security. Cryptology ePrint Archive, Paper 2019/582, 2019. https://eprint.iacr.org/2019/582.
60.
HofheinzDShoupV. Gnuc: a new universal composability framework. J Cryptol2015; 28: 423–508.
61.
LiaoKHammerMAMillerA. Ilc: A calculus for composable, computational cryptography. In: Proceedings of the 40th ACM SIGPLAN conference on programming language design and implementation, PLDI 2019, 2019, pp.640–654. New York, NY, USA: Association for Computing Machinery. ISBN 9781450367127.
62.
MaurerU. Constructive cryptography – a new paradigm for security definitions and proofs. In: Mödersheim S and Palamidessi C (eds) Theory of security and applications, 2012, pp.33–56. Berlin, Heidelberg: Springer Berlin Heidelberg. ISBN 978-3-642-27375-9.
63.
MaurerURennerR. Abstract cryptography. In: Chazelle B (ed) The second symposium on innovations in computer science, ICS 2011, 2011, pp.1–21. Tsinghua University Press.
64.
PatrignaniMWahbyRSKünnemanR. Universal composability is robust compilation. CoRR abs/1910.08634, 2019b.
Comon-LundhHCortierV. Computational soundness of observational equivalence. In: Proceedings of the 15th ACM conference on computer and communications security, CCS ’08, 2008, pp.109–118. New York, NY, USA: Association for Computing Machinery. ISBN 9781595938107. DOI: 10.1145/1455770.1455786.
67.
BackesMHofheinzDUnruhD. Cosp: A general framework for computational soundness proofs. In: Proceedings of the 16th ACM conference on computer and communications security, CCS ’09, 2009, pp.66–78. New York, NY, USA: Association for Computing Machinery. ISBN 9781605588940. DOI: 10.1145/1653662.1653672.
SkorstengaardLDevrieseDBirkedalL. Stktokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities. Proc ACM Program Lang2019; 3. DOI: 10.1145/3290332.
70.
JacobsKDevrieseDTimanyA. Purity of an ST monad: full abstraction by semantically typed back-translation. Proc ACM Program Lang2022; 6: 82:1–82:27.
71.
LADGORTMANNUNES. Full abstraction for expressiveness: history, myths and facts. Mathem Struct Comput Sci2016; 26: 639–654.
72.
ParrowJ. General conditions for full abstraction. Math Struct Comp Science2014; 26(4): 655–657.
73.
FelleisenM. On the expressive power of programming languages. Sci Comput Program1991; 17: 35–75.
74.
DenningDEDenningPJ. Certification of programs for secure information flow. Commun ACM1977; 20: 504–513.
75.
MyersAC. Jflow: Practical mostly-static information flow control. In: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’99, 1999, pp.228–241. New York, NY, USA: Association for Computing Machinery. ISBN 1581130953.
76.
PatrignaniMMartinEMDevrieseD. On the semantic expressiveness of recursive types. Proc ACM Program Lang2021; 5(POPL): 1–29. DOI: 10.1145/3434302.
77.
PatrignaniMGargD. Robustly Safe Compilation. In: Caires L (ed) Programming languages and systems, 2019, pp.469–498. Cham: Springer International Publishing. ISBN 978-3-030-17184-1.
78.
PatrignaniMAgtenPStrackxR, et al.Secure compilation to protected module architectures. ACM Trans Program Lang Syst2015; 37: 6:1–6:50.
79.
CauligiSDisselkoenCMoghimiD, et al.SoK: Practical foundations for software spectre defenses. In: 2022 IEEE symposium on security and privacy (SP), 2022 pp.666–680. DOI: 10.1109/SP46214.2022.9833707.
80.
BaecherPBrzuskaCFischlinM. Notions of black-box reductions, revisited. In: Sako K and Sarkar P (eds) Advances in cryptology - ASIACRYPT 2013, 2013, pp.296–315. Berlin, Heidelberg: Springer Berlin Heidelberg. ISBN 978-3-642-42033-7.
81.
ReingoldOTrevisanLVadhanS. Notions of reducibility between cryptographic primitives. In: Naor M (ed) Theory of cryptography, 2004, pp.1–20. Berlin, Heidelberg: Springer Berlin Heidelberg. ISBN 978-3-540-24638-1.
