Month: November 2024

Introduction

The security of Bitcoin, and other blockchains, such as Liquid, hinges on the use of digital signatures algorithms such as ECDSA and Schnorr signatures. A C library called libsecp256k1, named after the elliptic curve that the library operates on, is used by both Bitcoin Core and Liquid, to provide these digital signature algorithms. These algorithms make use of a mathematical computation called a modular inverse, which is a relatively expensive component of the computation.

In “Fast constant-time gcd computation and modular inversion,” Daniel J. Bernstein and Bo-Yin Yang develop a new modular inversion algorithm. In 2021, this algorithm, referred to as “safegcd,” was implemented for libsecp256k1 by Peter Dettman. As part of the vetting process for this novel algorithm, Blockstream Research was the first to complete a formal verification of the algorithm’s design by using the Coq proof assistant to formally verify that the algorithm does indeed terminate with the correct modular inverse result on 256-bit inputs.

The Gap between Algorithm and Implementation

The formalization effort in 2021 only showed that the algorithm designed by Bernstein and Yang works correctly. However, using that algorithm in libsecp256k1 requires implementing the mathematical description of the safegcd algorithm within the C programming language. For example, the mathematical description of the algorithm performs matrix multiplication of vectors that can be as wide as 256 bit signed integers, however the C programming language will only natively provide integers up to 64 bits (or 128 bits with some language extensions).

Implementing the safegcd algorithm requires programming the matrix multiplication and other computations using C’s 64 bit integers. Additionally, many other optimizations have been added to make the implementation fast. In the end, there are four separate implementations of the safegcd algorithm in libsecp256k1: two constant time algorithms for signature generation, one optimized for 32-bit systems and one optimized for 64-bit systems, and two variable time algorithms for signature verification, again one for 32-bit systems and one for 64-bit systems.

Verifiable C

In order to verify the C code correctly implements the safegcd algorithm, all the implementation details must be checked. We use Verifiable C, part of the Verified Software Toolchain for reasoning about C code using the Coq theorem prover.

Verification proceeds by specifying preconditions and postconditions using separation logic for every function undergoing verification. Separation logic is a logic specialized for reasoning about subroutines, memory allocations, concurrency and more.

Once each function is given a specification, verification proceeds by starting from a function’s precondition, and establishing a new invariant after each statement in the body of the function, until finally establishing the post condition at the end of the function body or the end of each return statement. Most of the formalization effort is spent “between” the lines of code, using the invariants to translate the raw operations of each C expression into higher level statements about what the data structures being manipulated represent mathematically. For example, what the C language regards as an array of 64-bit integers may actually be a representation of a 256-bit integer.

The end result is a formal proof, verified by the Coq proof assistant, that libsecp256k1’s 64-bit variable time implementation of the safegcd modular inverse algorithm is functionally correct.

Limitations of the Verification

There are some limitations to the functional correctness proof. The separation logic used in Verifiable C implements what is known as partial correctness. That means it only proves the C code returns with the correct result if it returns, but it doesn’t prove termination itself. We mitigate this limitation by using our previous Coq proof of the bounds on the safegcd algorithm to prove that the loop counter value of the main loop in fact never exceeds 11 iterations.

Another issue is that the C language itself has no formal specification. Instead the Verifiable C project uses the CompCert compiler project to provide a formal specification of a C language. This guarantees that when a verified C program is compiled with the CompCert compiler, the resulting assembly code will meet its specification (subject to the above limitation). However this doesn’t guarantee that the code generated by GCC, clang, or any other compiler will necessarily work. For example, C compilers are allowed to have different evaluation orders for arguments within a function call. And even if the C language had a formal specification any compiler that isn’t itself formally verified could still miscompile programs. This does occur in practice.

Lastly, Verifiable C doesn’t support passing structures, returning structures or assigning structures. While in libsecp256k1, structures are always passed by pointer (which is allowed in Verifiable C), there are a few occasions where structure assignment is used. For the modular inverse correctness proof, there were 3 assignments that had to be replaced by a specialized function call that performs the structure assignment field by field.

Summary

Blockstream Research has formally verified the correctness of libsecp256k1’s modular inverse function. This work provides further evidence that verification of C code is possible in practice. Using a general purpose proof assistant allows us to verify software built upon complex mathematical arguments.

Nothing prevents the rest of the functions implemented in libsecp256k1 from being verified as well. Thus it is possible for libsecp256k1 to obtain the highest possible software correctness guarantees.

This is a guest post by Russell O’Connor and Andrew Poelstra. Opinions expressed are entirely their own and do not necessarily reflect those of BTC Inc or Bitcoin Magazine.

Follow Nikolaus On X Here

Bitcoin and open-source companies are some of the most exciting and innovative companies out there today. There are a handful of companies I personally think are going to exponentially grow as bitcoin increases in price and becomes a more established asset class, and if investing in them was available to non-accredited bitcoiners like me, it would be a no-brainer.

But today, that may have just changed. Timestamp, a new platform that allows accredited and nonaccredited investors to invest in Bitcoin and open-source companies, has officially launched. Timestamp promises users they can invest in Bitcoin companies with “low investment minimums” where users can review offerings, connect directly with the founders of these companies, and explore curated opportunities. Sounds pretty cool!

The idea of making investing in Bitcoin and open-source companies more accessible to plebs really interests me, and I feel that many other Bitcoiners would agree. After working in this industry for a few years, I’ve definitely noticed that finding funding to support open-source companies and projects can be pretty difficult. But a platform that allows a lot more people to join in on investing in and supporting these companies could really be a game changer.

At launch, users can now invest in the first batch of Bitcoin companies on the platform:

CASCDR — a suite of AI services payable in Bitcoin

Jippi — a gamified education app that helps Bitcoin beginners learn and earn

Lightning Bounties — a Github-integrated platform that rewards software developers with Bitcoin for their contributions

Shopstr — a global, decentralized marketplace built on Nostr

Sovereign — a wallet built for the Bitcoin standard

I’ll definitely be paying attention to what other companies are added to this platform in the future, and I think you should too.

Over three years ago, I asked Timestamp’s founder and CEO, Dr. Arman Meguerian, to speak with me on stage at the Bitcoin 2021 Conference in Miami, and he joined me for a great conversation on Bitcoin maximalism with a few other great Bitcoiners. I am really excited and happy to see him launch this company after building it quietly through the bear market these last couple years, and looking forward to seeing all they achieve!

This article is a Take. Opinions expressed are entirely the author’s and do not necessarily reflect those of BTC Inc or Bitcoin Magazine.

Newmarket Capital recently closed the first investment deal for its new Battery Finance loan strategy, which enables borrowers to incorporate bitcoin into long-term financing structures as collateral.

On November 7, 2024, Newmarket Capital, an institutional capital manager and Registered Investment Adviser completed a refinancing for the Bank Street Court apartment in Old City, Philadelphia, PA. The loan was collateralized by both the building and approximately 20 bitcoin.

Newmarket Capital CEO Andrew Hohns is excited about not only setting his company’s new strategy in motion but the symbolism in the deal.

“It’s a building that is located less than half a block away from the first bank of the United States,” Hohns told Bitcoin Magazine. “Philadelphia has had a lot of firsts and innovations over the years, and we’re proud to contribute another one to the list.”

How The Battery Finance Strategy Works

Battery Finance enables bitcoin to be used as 10% to 30% of the collateral for loans alongside traditional assets. To bring this new strategy to life, Newmarket Capital partnered with Ten 31 to establish Battery Finance, a majority-owned subsidiary of Newmarket Capital that utilizes bitcoin in financing structures.

Unlike other lending companies that let clients borrow against bitcoin with a risk of liquidation in the event that bitcoin’s price drops below a certain threshold, Newmarket Capital removes the risk and offers loan structures without a mark-to-market trigger.

“As lenders, we are constructive on the long-term value of bitcoin and comfortable recognizing bitcoin as collateral without mark-to-market risk,” said Hohns.

“We achieve this by incorporating bitcoin as a component of a broader collateral package alongside traditionally financeable assets. In this way, we have improved our downside through the introduction of bitcoin, an uncorrelated element — an asset that has had such a strong history of appreciation over time — in the collateral package.”

Deals that employ this strategy can be structured differently. In some cases, a borrower can use bitcoin they’re already holding as collateral for a loan, while, in other cases, Newmarket Capital and the borrower purchase bitcoin as part of the loan’s structure. The latter is how the loan for the Bank Street Court building was structured.

“It’s a $16.5 million building, and we offered the building owner a $12.5 million loan,” explained Hohns.

“The use of proceeds was to pay off the existing financing, which was $9 million, to provide them with approximately two million dollars of CapEx for certain improvements to the property they wanted to make,” he added.

“With the remaining $1.5 million dollars, we purchased just shy of twenty bitcoin as part of our combined collateral package.”

(At the time of writing, that bitcoin had already appreciated 30% in value since it was purchased for the loan.)

Unlike traditional loans which often lock borrowers in with prepayment penalties or a make-

whole, the Bank Street Court financing can be paid off at any time with no penalty. To allow for this outcome, the borrower and the lender align to share appreciation on the upside from the bitcoin over the life of the loan.

The longer the loan is outstanding, the greater the share of bitcoin appreciation that vests for the borrower, incentivizing borrowers to take a long term view on the bitcoin.

Although the loan can be repaid at any time and the building released, the earliest that the bitcoin can be wound down is four years, in line with bitcoin’s four year rhythm. The loan carries a single digit interest rate and has a maturity of 10 years.

Bringing Forward Bitcoin’s Value

Hohns, a Bitcoiner himself, understands that other Bitcoiners have a low time preference, that they prioritize future economic well-being over more immediate gratification. However, he acknowledges that there are limits to this approach, which is why Newmarket Capital created the Battery Finance strategy.

“The lowest time preference is not feasible for humans, because we have a finite life,” he said.

“There’s a point where we want to accomplish things with our lives. We want to grow our business or start a new business or just do the things that we all have passion for, like opening up a MakerSpace or a brewery or a bookstore — whatever the case might be. If you’re just HODLing the Bitcoin, you’re deferring those dreams,” he added.

“By offering this financing tool, we can essentially serve as a mechanism to transform those time preferences, to bring forward the appreciation of the bitcoin by offering a significant amount of financing to accomplish whatever the real world goals borrowers have.”

Target Borrowers

Battery Finance is currently focused on working with borrowers who are interested in acquiring or refinancing commercial properties.

“For the time being, we’re inviting interest around loans that are, generally speaking, $10 million to $30 million dollars, which include 10% to 30% percent bitcoin with 70% to 90% percent traditionally-financeable income-producing assets,” explained Hohns.

“This is a tool for both asset owners that want to redenominate some of the equity in their

existing portfolio into bitcoin and its also a tool for Bitcoiners who want to obtain stable long-term financing supported in part by their bitcoin to acquire assets in the real world. This way, they can generate income and accomplish their goals while remaining invested in bitcoin.”

In time, Battery Finance plans to service a broader range of customers.

“We see broad applicability for this lending structure, including, over time, to people that are at different phases of their Bitcoin savings journeys,” said Hohns. “I hope that these kinds of products will develop into solutions that enable people to do things like finance a house or automobile with their bitcoin.”