{"id":2377,"date":"2019-03-15T11:59:53","date_gmt":"2019-03-14T22:59:53","guid":{"rendered":"http:\/\/www.talkcrypto.org\/blog\/?p=2377"},"modified":"2021-06-07T12:10:52","modified_gmt":"2021-06-07T00:10:52","slug":"static-and-symbolic-analysis","status":"publish","type":"post","link":"https:\/\/www.talkcrypto.org\/blog\/2019\/03\/15\/static-and-symbolic-analysis\/","title":{"rendered":"Static and Symbolic Analysis"},"content":{"rendered":"\n

Static Analysis<\/h4>\n\n\n\n

Static analysis can be described as a way to test code without actually executing it. The idea here is to use a computer program to analyse a program’s source code without running it.<\/p>\n\n\n\n

Static analysis has a few sub components such as Flow Analysis. This tracks how values might flow between the different memory relocations in a program. Tainted Flow Analysis is often referred to where untrusted input is considered tainted, eg input from a user and conversely, hardcoded values or constants are untainted.<\/p>\n\n\n\n

Flow Analysis can have “sensitivity” added to increase the precision and also to reduce false positives. It basically accounts for variables whose contents change, typically by using extra qualifiers.<\/p>\n\n\n\n

Context Sensitivity Analysis is another sub component of Static Analysis where calling other functions can cause false positives. “So context sensitive analysis solves this problem by distinguishing call sites in some way, so that we don’t allow a call at one place to return it’s value to another call.”<\/em><\/p>\n\n\n\n

Symbolic Analysis<\/h4>\n\n\n\n

Symbolic execution aims to generalise testing so that instead of testing with actual values, tests are run with variables. The image below explains it best.<\/p>\n\n\n\n

\"\"<\/figure><\/div>\n\n\n\n

Concolic testing is another term often thrown in when discussing symbolic execution or symbolic analysis. The word concolic is a portmanteau of concrete and symbolic and is a hybrid software verification technique that performs symbolic execution, a classical technique that treats program variables as symbolic variables, along a concrete execution (testing on particular inputs) path.<\/p>\n\n\n\n

For more information, check out this Coursera course on Software Security<\/a><\/p>\n\n\n\n

What does this have to do with Blockchain? The main language of smart contracts in Ethereum is Solidity and the language is still relatively immature. There are a bunch of code analysers though to help find bugs in your smart contracts. The options are as follows:<\/p>\n\n\n\n