* . *
  • About
  • Advertise
  • Privacy & Policy
  • Contact
Thursday, June 5, 2025
Earth-News
  • Home
  • Business
  • Entertainment
    Fox News Entertainment Newsletter: Celebrities mentioned during Diddy’s high-profile sex trafficking trial – Fox News

    Fox News Entertainment Newsletter: Celebrities mentioned during Diddy’s high-profile sex trafficking trial – Fox News

    ‘Sinners,’ starring Michael B. Jordan, is now streaming on Prime Video – About Amazon

    Experience the Thrills of ‘Sinners’ Starring Michael B. Jordan – Now Streaming on Prime Video!

    California Mid-State Fair announces entertainment lineups for Frontier and Mission stages – KSBY News

    Exciting Entertainment Lineup Unveiled for California Mid-State Fair’s Frontier and Mission Stages!

    Spotify & OpenAI: Will Gen AI ‘Hollow Out’ Entertainment? – Technology Magazine

    Will Generative AI Transform the Future of Entertainment

    Author Richard Russo Will Speak At Sandwich Town Hall – CapeNews.net

    Join Us for an Inspiring Evening with Author Richard Russo at Sandwich Town Hall!

    Entertainment Partners Acquires CASHét, Digital Payments Vendor for Productions – Variety

    Entertainment Partners Acquires CASHét, Digital Payments Vendor for Productions – Variety

  • General
  • Health
  • News

    Cracking the Code: Why China’s Economic Challenges Aren’t Shaking Markets, Unlike America’s” – Bloomberg

    Trump’s Narrow Window to Spread the Truth About Harris

    Trump’s Narrow Window to Spread the Truth About Harris

    Israel-Gaza war live updates: Hamas leader Ismail Haniyeh assassinated in Iran, group says

    Israel-Gaza war live updates: Hamas leader Ismail Haniyeh assassinated in Iran, group says

    PAP Boss to Niger Delta Youths, Stay Away from the Protest

    PAP Boss to Niger Delta Youths, Stay Away from the Protest

    Court Restricts Protests In Lagos To Freedom, Peace Park

    Court Restricts Protests In Lagos To Freedom, Peace Park

    Fans React to Jazz Jennings’ Inspiring Weight Loss Journey

    Fans React to Jazz Jennings’ Inspiring Weight Loss Journey

    Trending Tags

    • Trump Inauguration
    • United Stated
    • White House
    • Market Stories
    • Election Results
  • Science
  • Sports
  • Technology
    Domo to Participate in the D.A. Davidson Technology Summit – Business Wire

    Domo Set to Shine at the D.A. Davidson Technology Summit!

    When fiction becomes fact: 3 pieces of modern technology inspired by Star Trek – Redshirts Always Die

    From Screen to Reality: 3 Modern Technologies Inspired by Star Trek

    The Isfahan Center for Nuclear Technology – UCF, ZPP, and IRR10 – Alma Research and Education Center

    Exploring the Isfahan Center for Nuclear Technology: Innovations and Insights from UCF, ZPP, and IRR10

    Inside the tedious effort to tally AI’s energy appetite – MIT Technology Review

    Inside the tedious effort to tally AI’s energy appetite – MIT Technology Review

    Finland Set to Lead EU Quantum Technology Defense Project – IoT World Today

    Finland Set to Lead EU Quantum Technology Defense Project – IoT World Today

    AI for lawyers: Win back your time using technology – nationaljurist.com

    Reclaim Your Time: How AI is Transforming the Legal Profession

    Trending Tags

    • Nintendo Switch
    • CES 2017
    • Playstation 4 Pro
    • Mark Zuckerberg
No Result
View All Result
  • Home
  • Business
  • Entertainment
    Fox News Entertainment Newsletter: Celebrities mentioned during Diddy’s high-profile sex trafficking trial – Fox News

    Fox News Entertainment Newsletter: Celebrities mentioned during Diddy’s high-profile sex trafficking trial – Fox News

    ‘Sinners,’ starring Michael B. Jordan, is now streaming on Prime Video – About Amazon

    Experience the Thrills of ‘Sinners’ Starring Michael B. Jordan – Now Streaming on Prime Video!

    California Mid-State Fair announces entertainment lineups for Frontier and Mission stages – KSBY News

    Exciting Entertainment Lineup Unveiled for California Mid-State Fair’s Frontier and Mission Stages!

    Spotify & OpenAI: Will Gen AI ‘Hollow Out’ Entertainment? – Technology Magazine

    Will Generative AI Transform the Future of Entertainment

    Author Richard Russo Will Speak At Sandwich Town Hall – CapeNews.net

    Join Us for an Inspiring Evening with Author Richard Russo at Sandwich Town Hall!

    Entertainment Partners Acquires CASHét, Digital Payments Vendor for Productions – Variety

    Entertainment Partners Acquires CASHét, Digital Payments Vendor for Productions – Variety

  • General
  • Health
  • News

    Cracking the Code: Why China’s Economic Challenges Aren’t Shaking Markets, Unlike America’s” – Bloomberg

    Trump’s Narrow Window to Spread the Truth About Harris

    Trump’s Narrow Window to Spread the Truth About Harris

    Israel-Gaza war live updates: Hamas leader Ismail Haniyeh assassinated in Iran, group says

    Israel-Gaza war live updates: Hamas leader Ismail Haniyeh assassinated in Iran, group says

    PAP Boss to Niger Delta Youths, Stay Away from the Protest

    PAP Boss to Niger Delta Youths, Stay Away from the Protest

    Court Restricts Protests In Lagos To Freedom, Peace Park

    Court Restricts Protests In Lagos To Freedom, Peace Park

    Fans React to Jazz Jennings’ Inspiring Weight Loss Journey

    Fans React to Jazz Jennings’ Inspiring Weight Loss Journey

    Trending Tags

    • Trump Inauguration
    • United Stated
    • White House
    • Market Stories
    • Election Results
  • Science
  • Sports
  • Technology
    Domo to Participate in the D.A. Davidson Technology Summit – Business Wire

    Domo Set to Shine at the D.A. Davidson Technology Summit!

    When fiction becomes fact: 3 pieces of modern technology inspired by Star Trek – Redshirts Always Die

    From Screen to Reality: 3 Modern Technologies Inspired by Star Trek

    The Isfahan Center for Nuclear Technology – UCF, ZPP, and IRR10 – Alma Research and Education Center

    Exploring the Isfahan Center for Nuclear Technology: Innovations and Insights from UCF, ZPP, and IRR10

    Inside the tedious effort to tally AI’s energy appetite – MIT Technology Review

    Inside the tedious effort to tally AI’s energy appetite – MIT Technology Review

    Finland Set to Lead EU Quantum Technology Defense Project – IoT World Today

    Finland Set to Lead EU Quantum Technology Defense Project – IoT World Today

    AI for lawyers: Win back your time using technology – nationaljurist.com

    Reclaim Your Time: How AI is Transforming the Legal Profession

    Trending Tags

    • Nintendo Switch
    • CES 2017
    • Playstation 4 Pro
    • Mark Zuckerberg
No Result
View All Result
Earth-News
No Result
View All Result
Home Technology

F* – A Proof-Oriented Programming Language

May 16, 2024
in Technology
F* – A Proof-Oriented Programming Language
Share on FacebookShare on Twitter

F* (pronounced F star) is a general-purpose proof-oriented
programming language, supporting both purely functional and
effectful programming. It combines the expressive power of dependent
types with proof automation based on SMT solving and tactic-based
interactive theorem proving.

F* programs compile, by default, to OCaml. Various fragments of F*
can also be extracted to F#, to C or Wasm by a tool
called KaRaMeL,
or to assembly using
the Vale
toolchain. F* is implemented in F* and bootstrapped using OCaml.

F* is open source on GitHub and is under
active development by Microsoft Research,
Inria, and by the community.

F* is distributed under the Apache 2.0 license.
Binaries for Windows, Linux, and Mac OS X are posted regularly on the releases page on GitHub.
You can also install F* from OPAM, Docker, Nix, or build it from sources, by following the instructions in INSTALL.md.

An online
book Proof-oriented
Programming In F* is being written and regular updates are
posted online. You probably want to read it while trying out
examples and exercises in your browser by clicking the image below.

F* Tutorial

Low*

We also have a
tutorial that covers Low*, a low-level subset of F*, which can be compiled to C by KaRaMeL.

Course Material

F* courses are often taught at various seasonal schools. Lectures and course materials for some of them are
also a useful resource.

Embedding Proof-oriented Programming Languages in F*)

Online lectures at the Oregon Programming Language Summer School (2021): Lecture notes, slides, code

Formal Verification with F* and Meta-F*

Lectures and tutorial at ECI 2019: Lecture notes, slides, code

Verifying Low-Level Code for Correctness and Security

Lectures at the Oregon Programming Language Summer School (2019): Lecture notes, slides, code

Program Verification with F*

Course at 2018 EUTypes Summer School,
8-12 August, 2018, Ohrid, Macedonia Course material

F* is used in several projects in both industrial and academic settings.
We list a few of them here. If you are using F* in your project, please
let us know by writing to the fstar-mailing-list.

Project Everest

Project Everest is an umbrella project that develops high-assurance
secure communication software in F*. A big part of the development of F* has been motivated by the scenarios
that Project Everest targets. Several offshoots from Project Everest continue as their own projects, including
some of those listed below.

HACL*, ValeCrypt, and EverCrypt

HACL* is a library of high-assurance cryptographic primitives, written in F* and extracted to C.
ValeCrypt provides formally proven implementations of cryptographic primitives in Vale,
a framework for verified assembly language programming embedded in F*.
EverCrypt combines them into a single cryptographic provider.
Code from these projects is now used in production in several projects,
including Mozilla Firefox,
the Linux kernel,
Python,
mbedTLS, the Tezos blockchain,
the ElectionGuard electronic voting SDK, and the Wireguard VPN.

EverParse

EverParse is a parser generator for binary formats that produces C code extracted from formally proven F*.
Parsers from EverParse are used in production in several projects, including in Windows Hyper-V,
where every network packet passing through the Azure cloud platform is parsed and validated first by code generated by EverParse. EverParse is also used in other
production settings, including ebpf-for-windows.

F* is an active topic of research, both in the programming languages and formal methods community,
as well as from an application perspective in the security and systems communities.
We list a few of them below, with full citations to these papers available in this bibliography.
If you would like your paper included in this list, please contact [email protected].

The Design of F* and its DSLs

Dependent
Types and Multi-monadic Effects in F* (POPL 2016) This
is the canonical reference describing the F* system. The
language has evolved in significant ways since 2016,
however, its core design and implementation is based on
this paper.

Verified
Low-level Programming Embedded in F* (ICFP 2017) which
describes the Low* fragment of F* which is a low-level
subset of F* that can be compiled to C by KaRaMeL.

A
Verified, Efficient Embedding of a Verifiable Assembly
Language (POPL 2019) which describes the Vale
language, a verified assembly language embedded in F*.

Meta-F*:
Proof Automation with SMT, Tactics, and Metaprograms
(ESOP 2019) which describes MetaF*, a metaprogramming
system within F* used to implement various aspects of F*,
ranging from its tactic engine to its support for
typeclasses.

Programming
and Proving with Indexed Effects (TR 2021) which
describes the design of F*’s support for user-defined
effects and provides a calculus that describes the logical
core of F*.

Steel:
Proof-oriented Programming in a Dependently Typed
Concurrent Separation Logic (ICFP 2021), which
describes the Steel language and its use of the SteelCore
concurrent separation logic for proofs of imperative
programs with various forms of concurrency.

Semantics and Effects

Verifying
Higher-order Programs with the Dijkstra Monad (PLDI
2013), which introduces the concept of the Dijkstra monad,
a core feature of F*’s system of effects.

Dijkstra
Monads for Free (POPL 2017), which shows how to
automatically derive Dijkstra monads for a class of
computational monads using a continuation-passing
transformation

A Monadic
Framework for Relational Verification: Applied to Information
Security, Program Equivalence, and Optimizations (CPP
2018), which builds on the Dijkstra Monads for Free work to
construct a framework for proving properties that relate
multiple programs or program executions.

Dijkstra Monads
for All (ICFP 2019), which generalizes the notion of a
Dijkstra monad and shows how to systematically relate
computational and specificational monads via monad morphisms.

Recalling a
Witness: Foundations and Applications of Monotonic
State (POPL 2018), which describes the design of a
program logic for reasoning about programs whose state
evolves monotonically, e.g., where the state is an
append-only log. This logic underpins both Low* and
Steel.

SteelCore:
An Extensible Concurrent Separation Logic for Effectful
Dependently Typed Programs (ICFP 2020), which describes
the SteelCore concurrent separation logic, the basis of the
Steel DSL.

Applications in Security and Cryptography

Many papers applying F* in security and cryptography can be
found in
the Project
Everest bibliography. We mention a few prominent ones here
as well as other applications not related to Project Everest.

WYS*: A DSL for
Verified Secure Multi-party Computations (POST 2017),
which describes the WYS* language, a domain-specific language
for writing verified mixed-mode secure multi-party
computations.

Implementing
and Proving the TLS 1.3 Record Layer(S&P 2017), which
describes a verified implementaion of the TLS-1.3 record layer
in Low*.

HACL*: A
Verified Modern Cryptographic Library (CCS 2017), which
describes HACL*, a verified cryptographic library
implemented in Low*.

Formally
Verified Cryptographic Web Applications in WebAssembly
(S&P 2019), which develops LibSignal*, an implementation
of the Signal protocol in F* using HACL*, compiled to Wasm
by KaRaMeL.

EverCrypt:
A Fast, Verified, Cross-Platform Cryptographic
Provider (S&P 2020), a crypto provider combining C and
assembly code from HACL* and Vale, as well as some
applications built on top of it, including a verified
high-performance Merkle tree that was used in an initial
version of Microsoft Azure CCF.

HACL×N:
Verified Generic SIMD Crypto (for all your favorite
platforms) (CCS 2020), which metaprograms vectorized
versions of cryptographic primitives, enabling a
“write-once, get vectorized versions for free” style.

A
Security Model and Fully Verified Implementation for the IETF
QUIC Record Layer (S&P 2021), a verified implementation of
the QUIC record layer in Low* combined with the protocol logic
implemented in Dafny.

DICE*:
A Formally Verified Implementation of DICE Measured Boot
(USENIX Security 2021), which proves the correctness &
security of the DICE measured boot protocol for
micro-controllers, implemented in Low*, using EverCrypt and
EverParse.

DY*:
A Modular Symbolic Verification Framework for Executable
Cryptographic Protocol Code (Euro S&P 2021), a framework
for type-based symbolic security analysis of cryptographic
protocol implementations developed in F*.

A
Tutorial-Style Introduction to DY* (LNCS 2021), which is, yes,
a tutorial-style introduction to DY*.

An
In-Depth Symbolic Security Analysis of the ACME
Standard (CCS 2021), which proves the security of a
model of the ACME certificate issuance and management
protocol using DY*.

Noise*:
A Library of Verified High-Performance Secure Channel Protocol
Implementations (S&P 2022), which metaprograms provably
secure implementations for a family of secure channel
protocols.

TreeSync:
Authenticated Group Management for Messaging Layer
Security (USENIX Security 2023), a reference
implementation of MLS in F*, proven secure using the DY*
framework.

Modularity,
Code Specialization, and Zero-Cost Abstractions for Program
Verification (ICFP 2023), which describes
proof-engineering techniques used in HACL* for generic
implementations of cryptographic constructions that can be
specialized repeatedly to many concrete implementations in
C. The techniques used here led to the adoption of verified
cryptographic code into the libraries of the Python
programming language.

Verifying
Indistinguishability of Privacy-Preserving Protocols
(OOPSLA 2023), which provides a library called Waldo in F*
that enables proofs of indistinguishability over traces of
communication in networking protocols.

Comparse:
Provably Secure Formats for Cryptographic Protocols (CCS
2023), which provides a parsing library for data formats that
are appropriate for use with symbolic protocol
analyzers. Comparse provides bit-level precise accounting of
formats allowing the DY* protocol analysis framework to reason
about concrete messages and identify protocol flaws that it
previously would have missed.

Applications in Systems

Provably-Safe
Multilingual Software Sandboxing using WebAssembly (USENIX
2022), which describes a verified implementation of a sandbox
for WebAssembly modules in Low* and Rust.

FastVer:
Making Data Integrity a Commodity (SIGMOD 2021), which
formalizes a protocol for data integrity monitoring in F*.

FastVer2:
A Provably Correct Monitor for Concurrent, Key-Value
Stores (CPP 2022), which proves the correctness of a
low-level, concurrent implementation of the FastVer protocol
in Steel.

Applications in Parsing

EverParse:
Verified Secure Zero-Copy Parsers for Authenticated
Message Formats (USENIX Security 2019), which
describes the EverParse parser generator for parsing
binary formats, producing C code.

Hardening
Attack Surfaces with Formally Proven Binary Format
Parsers (PLDI 2022), which uses EverParse to harden
network packet parsers in Windows Network Virtualization
and Hyper-V.

ASN1*:
Provably Correct Non-Malleable Parsing for ASN.1 DER
(CPP 2022), which formalizes the ASN.1 DER format in F*
and proves the correctness of a parser for it in
EverParse.

Applications in Programming, Program Proof, and Program Analysis

Verified
Compilation of Space-Efficient Reversible Circuits (CAV
2018), which presents ReVerC, a compiler for reversible
circuits proven correct in F*.

Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
(VSTTE 2020), which develops verified transformations
for assembly programs in the Vale framework.

Statically
verified refinements for multiparty protocols (OOPSLA
2020), which presents Session*, a session-typed programming
language for multiparty protocols, formalized in F*.

Verified
Functional Programming of an Abstract Interpreter (SAS
2021), which develops an abstract interpretation framework for
an imperative language with a very compact proof of soundness
developed in F*.

Catala:
a programming language for the law (ICFP 2021), where
core parts of the compiler are formalized and proven correct
in F*.

Verification of
a Merkle Patricia Tree Library Using F*, which ports a
Merkle tree library from OCaml to F*, finds and fixes a bug,
and eventually proves it correct.

Certified
mergeable replicated data types (PLDI 2022), which
presents PEEPUL, a framework in which to build replicated data
types for use in distributed programming, formalized in
F*.

Aeneas:
Rust verification by functional translation (ICFP
2022), which translates Rust into pure F* enabling
functional correctness proofs.

Q*:
Implementing Quantum Separation Logic in F* (PlanQC 2022),
which adapts the SteelCore separation logic for use with a
quantum programming language.

Pipit:
Reactive Systems in F* (Extended Abstract) (TyDe 2023),
which describes a embedded DSL for verifying reactive systems.

Securing
Verified IO Programs Against Unverified Code in F*
(POPL 2024), which presents SCIO*, a formally secure
compilation framework for statically verified programs
performing input-output (IO).

Miscellaneous

A
Theorem Proving Approach to Programming Language Semantics
(ICSE-SEET 2023), which reports on experiences teaching
operational, denotational, and axiomatic semantics to students
using F*.

Papers about an older version of F*

The first paper to introduce a system called F* was in
2011. Although the current version of F* was redesigned and
implemented in 2015, we include some of these older papers here
for completeness.

Secure
Distributed Programming with Value-dependent Types (ICFP
2011), a longer version of which also appeared
in JFP.

Self-certification:
bootstrapping certified typecheckers in F* with Coq (POPL
2012), which certifies the correctness of the F* typechecker by
programming it in F* itself and bootstrapping the process by
checking about 7GB of proof using Coq in about 24 machine-days
of compute time.

Fully
abstract compilation to JavaScript (POPL 2013), which
models a subset of JavaScript in F* and develops a secure
compiler from an ML-like language to JavaScript.

Gradual
typing embedded securely in JavaScript (POPL 2014),
which develops a source-to-source compiler for
JavaScript with defensive checks to ensure the soundness of
gradual typing in adversarial contexts, proven corrent in
F*.

Probabilistic
relational verification for cryptographic implementations
(POPL 2014), which develops RF*, a relational dialect of the
language useful for proving security properties like
noninterference and for game-based cryptographic proofs.

>>> Read full article>>>
Copyright for syndicated content belongs to the linked Source : Hacker News – https://www.fstar-lang.org/

Tags: ProgrammingProof-Orientedtechnology
Previous Post

SSE vs. SASE: Which One is Right for Your Business?

Next Post

You thought OpenStreetMap uses WGS84? No it doesn’t

Black-hole scattering calculations could shed light on gravitational waves – Physics World

Unlocking the Secrets of Gravitational Waves: The Role of Black-Hole Scattering Calculations

June 5, 2025
Fed: The Economy Is Slowing As ‘Companies Can’t Figure Out the Rules of This Tariff Game’ – Investopedia

Fed Signals Economic Slowdown: Companies Struggle to Navigate the Tariff Maze

June 5, 2025
Fox News Entertainment Newsletter: Celebrities mentioned during Diddy’s high-profile sex trafficking trial – Fox News

Fox News Entertainment Newsletter: Celebrities mentioned during Diddy’s high-profile sex trafficking trial – Fox News

June 5, 2025
Axxam and Molecular Health link on therapeutic target identification – Pharmaceutical Technology

Unlocking New Possibilities: Axxam and Molecular Health Collaborate on Innovative Therapeutic Target Identification

June 5, 2025
Opinion | The Right Is Getting Even More Regressive on Gender – The New York Times

Opinion | The Right Is Getting Even More Regressive on Gender – The New York Times

June 5, 2025
Capsol Technologies ASA: Two US engineering studies awarded – mature pipeline projects advancing – Cision News

Capsol Technologies ASA Secures Two Major US Engineering Studies, Advancing Promising Pipeline Projects!

June 5, 2025
Pittsburgh Steelers’ training camp opens July 23 – altoonamirror.com

Get Ready for Action: Pittsburgh Steelers’ Training Camp Kicks Off on July 23!

June 5, 2025
The Ecology of Visitation – National Park Service (.gov)

Exploring the Impact of Visitor Interactions on Natural Ecosystems

June 5, 2025
Students play with science at Camp Invention at School of Innovation – News-Herald

Unleashing Creativity: Students Dive into Science at Camp Invention!

June 5, 2025
Are cold plunges good for you? Here’s what the science says. – The Washington Post

Unlocking the Benefits of Cold Plunges: What Science Reveals!

June 5, 2025

Categories

Archives

June 2025
MTWTFSS
 1
2345678
9101112131415
16171819202122
23242526272829
30 
« May    
Earth-News.info

The Earth News is an independent English-language daily published Website from all around the World News

Browse by Category

  • Business (20,132)
  • Ecology (667)
  • Economy (682)
  • Entertainment (21,588)
  • General (15,263)
  • Health (9,724)
  • Lifestyle (684)
  • News (22,149)
  • People (682)
  • Politics (691)
  • Science (15,901)
  • Sports (21,186)
  • Technology (15,667)
  • World (668)

Recent News

Black-hole scattering calculations could shed light on gravitational waves – Physics World

Unlocking the Secrets of Gravitational Waves: The Role of Black-Hole Scattering Calculations

June 5, 2025
Fed: The Economy Is Slowing As ‘Companies Can’t Figure Out the Rules of This Tariff Game’ – Investopedia

Fed Signals Economic Slowdown: Companies Struggle to Navigate the Tariff Maze

June 5, 2025
  • About
  • Advertise
  • Privacy & Policy
  • Contact

© 2023 earth-news.info

No Result
View All Result

© 2023 earth-news.info

No Result
View All Result

© 2023 earth-news.info

Go to mobile version