With version 0.18.0 of clarity-repl and version 0.21.2 of Clarinet, we've added a new analysis pass to help ensure that your smart contracts are safe and secure. It's called the "check-checker", and this article will explain what it is and how it works.

In program analysis, we use the term, "tainted data" to describe any inputs to the program that come from an untrusted source, typically the users. Failure to properly manage this tainted data is the cause of most software vulnerabilities. A very simple case of unmanaged tainted data causing a problem in a Clarity smart contract could be something like this:

(define-public (transfer (token-id uint) (sender principal) (recipient principal))
    (nft-transfer? my-nft token-id sender recipient)
)

In the above contract, transfer is a public function, so all of the parameters are untrusted. The nft-transfer? call will fail if the sender does not actually own the NFT with the given ID, so we can ignore that for now. However, the developer probably did not intend to let anyone transfer NFTs belonging to others. What's missing is a check to verify that the transaction sender is the same as the sender argument to this function. Our new analysis pass is called the check-checker because it checks whether or not untrusted input has been checked. With the check-checker enabled, here's what you'll see:

TEST:17:36: WARNING: USE OF POTENTIALLY UNCHECKED DATA
(NFT-TRANSFER? MY-NFT TOKEN-ID SENDER RECIPIENT)
^~~~~~
TEST:16:43: NOTE: SOURCE OF UNTRUSTED INPUT HERE
(DEFINE-PUBLIC (TRANSFER (TOKEN-ID UINT) (SENDER PRINCIPAL) (RECIPIENT PRINCIPAL))
^~~~~~

‍

"Our new analysis pass is called the check-checker because it checks whether or not untrusted input has been checked."

To clear that warning, we need to add some kind of check on the untrusted input, sender, before using it in the nft-transfer?.

(define-public (transfer (token-id uint) (sender principal) (recipient principal))
    (begin
        (asserts! (is-eq tx-sender sender) (err u403))
        (nft-transfer? my-nft token-id sender recipient)
    )
)

How does it work?

There are three concepts that are important to the of analysis of tainted data:

1. Source: an untrusted input
2. Filter: an expression that checks a source, making it trusted
3. Sink: an expression that must not be passed untrusted data

In the above example, the source is the parameter sender, the filter is the asserts! expression and the sink is the nft-transfer? call. Sources of untrusted data are any inputs to public functions. This untrusted data spreads like fire through expressions where it is used, making them also untrusted (or tainted), until it is filtered.

(define-public (propagation (amount uint))    (stx-transfer? (+ u10 amount) (as-contract tx-sender) tx-sender))

In the above example, the input amount is a source of untrusted data. Since it is used, unchecked, in the + expression, that expression is now also untrusted, so this would trigger a check-checker warning on the call to stx-transfer?.

The original example demonstrates using asserts! to filter the untrusted data, but there are several other ways. Note that the system does not attempt to be smart enough to guarantee that the correct check is performed to filter the data, only that some check has been performed. It is up to the developer to ensure that the check is correct. The following expressions can be used as filters:

• if: When the condition of an if expression is tainted by a source, that source is considered filtered afterwards.
• and and or: Both of these logical expressions are executed lazily, so they impact control flow in the program. After an expression tainted by a source is used in an and or or expression, it is considered filtered.
• asserts!: When the boolean expression of an asserts! expression is tainted by a source, that source is considered filtered afterwards.

Sinks are places where we really need to make sure that untrusted data is not used. Sinks include all operations that have externally visible results:

Actions on Stacks wallets:

• stx-burn?
• stx-transfer?

Actions on fungible tokens:

• ft-burn?
• ft-mint?
• ft-transfer?

Actions on non-fungible tokens:

• nft-burn?
• nft-mint?
• nft-transfer?

Actions on persisted data:

Maps:

• map-delete
• map-insert
• map-set

Variables:

• var-set

In addition to those, the check-checker is also a bit opinionated and prefers that untrusted data be checked near the source, making the code more readable and maintainable. For this reason, it also requires that arguments passed into private functions must be checked and return values must be checked.

• Calls to private functions
• Return values

Finally, another opportunity for exploits shows up when contracts call functions from traits. Those traits are untrusted, just like other parameters to public functions, so they are also required to be checked.

• Dynamic contract calls (through traits)

Annotations

Since the check-checker cannot perfectly understand the code, there may be safe code that nevertheless triggers a warning from the check-checker — a false positive. False positives are like kryptonite to program analyzers because if developers see a bunch of invalid warnings, then they end up ignoring them altogether. To avoid this problem, we've added annotations that let developers tell the check-checker, "I know this looks dangerous, but trust me, I know what I'm doing."

;; #[allow(unchecked_data)]
(var-set myvar (+ amount u10))

This allow(unchecked_data) annotation indicates that the expression beginning on the following line should not be checked. No warnings will be reported for that line, so in the above example, even if amount has not been checked, there will be no warning. Note that the annotation is just a magic comment, so if you are not running the check-checker, it does not affect the code at all.

;; #[allow(unchecked_params)]
(define-private (my-func (amount uint))
    (if (< amount u10) amount u10)
)

The allow(unchecked_params) annotation specifies that the check-checker should not generate a warning if unchecked parameters are passed to the function defined on the next line. This can be very useful if a developer wants to define a private function that acts as a filter — taking unchecked data in, checking it, and returning trusted data. Remember that the return value from such a function will trigger a warning if it is unchecked.

Both of these annotations are currently a bit broad, in that they apply to all variables/parameters in the targeted expression/function. In future updates, these will be improved with more specific targeting.

Usage

To try the check-checker, you just need to enable the new analysis pass in your Clarinet.toml file:

[project]
name = "my-contract"
requirements = []
costs_version = 2
# analysis = ["check_checker"]  # <---- Add this line!
# Or this line to enable all analysis passes in the future
# analysis = ["all"]

[contracts.test]
path = "contracts/foo.clar"
depends_on = []

‍

Then, just call clarinet check as you always do, and you might see some new warnings from the check-checker.

Remember, this feature is new and is not intended to make any safety guarantees, but it should help. Several well-known vulnerabilities that we've seen in the past would've been caught by this new analysis. We at Hiro want to help you catch future vulnerabilities before they go live!

Now go and check it out (pun intended)! Please open issues for us on GitHub if you find any missing warnings or annoying false positives, and we'll continue to improve.

If you'd like to see the check-checker in action, you can also watch Brice give a demo of the Clarinet feature in a video on our YouTube channel.