todo: refactor this note
Information flow checks are a form of security checks that track where information is flowing from and to and under which circumstances. It can be performed as a dynamic check on a single execution (“taint tracking”) or as a static analysis that typically compares results on two or more executions.
A distinction is often made before “explicit” information flow (e.g., “x = y;”) and “implicit” information flow (e.g., “if y then x = 1;” which has an information flow from y to x even if y is False). This distinction reflects a classic weakness of taint tracking approaches that dynamically tag values with metadata during an execution and, because they are based on a single execution, are unable to accurately track information flows in the paths that are not executed.
Some topics are
- Declassification
- Cryptography
- Operating Systems
- Languages
- Type-based information flow checking
- Self-composition
- Hardware
- Systems
- Quantitative
Notes related to Information flow
Language based security, Non-interference, Non leakage, Self composition
Papers related to Information flow
- Verifying constant-time implementations [almeida:security:2016]
- Secure information flow by self composition [barthe:csfw:2004]
- Provably secure compilation of side-channel countermeasures. [barthe:iacr:2007]
- Secure information flow by self-composition [barthe:mscs:2011]
- SoK: Practical foundations for software Spectre defenses [cauligi:sandp:2022]
- Quantitative analysis of the leakage of confidential data [clark:entcs:2002]
- Hyperproperties [clarkson:jcs:2010]
- End-to-end verification of information flow security for C and assembly programs [costanzo:pldi:2016]
- Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level [daniel:sandp:2020]
- SecChisel: Language and tool for practical and scalable security verification of security-aware hardware architectures [deng:hasp:2019]
- A lattice model of secure information flow [denning:cacm:1976]
- Labels and event processes in the Asbestos operating system [efstathopoulos:sosp:2005]
- CommCSL: Proving information flow security for concurrent programs using abstract commutativity [eilers:pldi:2023]
- Verification of a practical hardware security architecture through static information flow analysis [ferraiuolo:asplos:2017]
- HyperFlow: A processor architecture for nonmalleable, timing-safe information flow security [ferraiuolo:ccs:2018]
- Secure information flow verification with mutable dependent types [ferraiuolo:dac:2017]
- Komodo: Using verification to disentangle secure-enclave hardware from software [ferraiuolo:sosp:2017]
- Solver-aided constant-time hardware verification [gleissenthall:ccs:2021]
- Security policies and security models [goguen:secpriv:1982]
- Unwinding and inference control [goguen:secpriv:1984]
- Testing noninterference, quickly [hritcu:icfp:2013]
- Machine assisted proof of ARMv7 instruction level isolation properties [khakpour:cpp:2013]
- Information flow control for standard OS abstractions [krohn:sosp:2007]
- Verifying the Microsoft Hyper-V hypervisor with VCC [leinenbach:fm:2009]
- Secure autonomous cyber-physical systems through verifiable information flow control [liu:cpsspc:2018]
- Quantifying information flow [lowe:csfw:2015]
- Controlling the what and where of declassification in language-based security [mantel:pls:2007]
- Preserving information flow properties under refinement [mantel:sp:2001]
- Product programs in the wild: Retrofitting program verifiers to check information flow security [marco:cav:2021]
- seL4: from general purpose to a proof of information flow enforcement [murray:secpriv:2013]
- Enforcing robust declassification [myers:csfw:2004]
- Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]
- Theoretical analysis of gate level information flow tracking [oberg:dac:2010]
- Noninterference, transitivity, and channel-control security policies [rushby:sri:1992]
- Declassification: Dimensions and principles [sabelfield:jcs:2009]
- Obtaining information leakage bounds via approximate model counting [saha:pldi:2023]
- Nickel: A framework for design and verification of information flow control systems [sigurbjarnarson:osdi:2018]
- On the foundations of quantitative information flow [smith:fossacs:2009]
- The Flask security architecture: System support for diverse security policies [spencer:security:1999]
- Complete information flow tracking from the gates up [tiwari:asplos:2009]
- Execution leases: A hardware-supported mechanism for enforcing strong non-interference [tiwari:isca:2009]
- Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security [tiwari:isca:2011]
- überSpark: Enforcing verifiable object abstractions for automated compositional security analysis of a hypervisor [vasudevan:usenix:2016]
- Relational test tables: A practical specification language for evolution and security [weigl:arxiv:2019]
- Robust declassification [zdancewic:csfw:2001]
- Observational determinism for concurrent program security [zdancewic:csfw:2003]
- Making information flow explicit in HiStar [zeldovich:osdi:2006]
- A hardware design language for timing-sensitive information flow security [zhang:asplos:2015]