F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, C or ASM code. This enables verifying the functional correctness and security of realistic applications. The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest. This includes verified implementations of TLS 1.2 and 1.3 and of the underlying cryptographic primitives. F*’s type system includes dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and interactive proofs.

References in zbMATH (referenced in 20 articles , 2 standard articles )

Showing results 1 to 20 of 20.
Sorted by year (citations)

  1. Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David: System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory (2020)
  2. Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
  3. Baillot, Patrick; Barthe, Gilles; Dal Lago, Ugo: Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs (2019)
  4. Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil: Dijkstra monads for free (2017)
  5. Bugliesi, Michele; Calzavara, Stefano; Focardi, Riccardo: Formal methods for web security (2017)
  6. Dagand, Pierre-Evariste: The essence of ornaments (2017)
  7. Harris, William R.; Jha, Somesh; Reps, Thomas W.; Seshia, Sanjit A.: Program synthesis for interactive-security systems (2017)
  8. Lepigre, Rodolphe: A classical realizability model for a semantical value restriction (2016)
  9. Lochbihler, Andreas: Probabilistic functions and cryptographic oracles in higher order logic (2016)
  10. McBride, Conor: I got plenty o’ nuttin’ (2016)
  11. Thiemann, Peter: A delta for hybrid type checking (2016)
  12. Yang, Yanpeng; Bi, Xuan; Oliveira, Bruno C.d. S.: Unified syntax with iso-types (2016)
  13. Bartoletti, Massimo; Castellani, Ilaria; Deniélou, Pierre-Malo; Dezani-Ciancaglini, Mariangiola; Ghilezan, Silvia; Pantovic, Jovanka; Pérez, Jorge A.; Thiemann, Peter; Toninho, Bernardo; Vieira, Hugo Torres: Combining behavioural types with security analysis (2015)
  14. Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Padovani, Luca; Yoshida, Nobuko: A gentle introduction to multiparty asynchronous session types (2015)
  15. Sattarzadeh, Behnam; Fallah, Mehran S.: Automated type-based analysis of injective agreement in the presence of compromised principals (2015)
  16. Lourenço, Luísa; Caires, Luís: Information flow analysis for valued-indexed data security compartments (2014)
  17. Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean: Secure distributed programming with value-dependent types (2013)
  18. Fournet, Cédric; Bhargavan, Karthikeyan; Gordon, Andrew D.: Cryptographic verification by typing for a sample protocol implementation (2011)
  19. Pfenning, Frank; Caires, Luis; Toninho, Bernardo: Proof-carrying code in a session-typed process calculus (2011)
  20. Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean: Secure distributed programming with value-dependent types (2011)

Further publications can be found at: https://www.fstar-lang.org/#papers