A more advanced mode of TSA operation is the safety-properties mode. TSA provides a set of special functions in FunC with specific meanings for the analyzer. These include contract method invocation functions (tsa_call_*_*), functions to enable/disable error detection (tsa_forbid_failures/tsa_allow_failures), and symbolic condition assertion functions (tsa_assert/tsa_assert_not). These functions allow the configuration of the analyzer to validate specific contract specifications. To operate in this mode, use tsa-safety-properties.jar or the -c option in the Docker container.
Safety properties of jetton wallets
Currently, this mode is used to implement a validation of the jetton-master contract to ensure compliance with a specification of the corresponding jetton-wallet. Violations of this specification can lead to either incorrect smart contract behavior or even intentional vulnerabilities designed to exploit users. In this mode, the analyzer accepts the address of a jetton-master contract as input and outputs a list of addresses to which token transfers are impossible.
Let’s consider operating in this mode with an example – the token EQAyQ-wYe8U5hhWFtjEWsgyTFQYv1NYQiuoNz6H3L8tcPG3g, a scam token that cannot be resold after purchase. Running the analyzer on this contract with the following command (for the macOS ARM platform):
docker run --platform linux/amd64 -it --rm ghcr.io/espritoxyz/tsa:latest -c -a EQAyQ-wYe8U5hhWFtjEWsgyTFQYv1NYQiuoNz6H3L8tcPG3g
returns the following output:
{
"analyzedAddress": "EQAyQ-wYe8U5hhWFtjEWsgyTFQYv1NYQiuoNz6H3L8tcPG3g",
"jettonWalletCodeHashBase64": "peaXBR8Ky/bgTbDDlWZHq9VS7ssYwHMFYXIRusEhmcc=",
"blacklistedAddresses": [
"0111011110011101110011001000000101010001001110001101100101010000000011100100010010011100010100101001000111100111111100010010011100111000110000100011110101010111010110110101001100010000000000000000111101101010001001010011101111010110000001110011100001001110",
"0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
]
}
The first address in this list corresponds to the STON.fi exchange router, where the token is hosted. This indicates that the token cannot be sold after purchase, confirming it as a scam token.