Jinsi ya kutumia Slither kupata hitilafu za mikataba mahiri

Solidity

mikataba mahiri

usalama

upimaji

Ya juu

Trailofbits

Building secure contracts

9 Juni 2020

7 dakika za kusoma

Jinsi ya kutumia Slither

Lengo la mafunzo haya ni kuonyesha jinsi ya kutumia Slither kupata hitilafu kiotomatiki kwenye mikataba mahiri.

Usakinishaji
Matumizi ya mstari wa amri
Utangulizi wa uchanganuzi tuli: Utangulizi mfupi wa uchanganuzi tuli
API: Maelezo ya API ya Python

Usakinishaji

Slither inahitaji Python >= 3.6. Inaweza kusakinishwa kupitia pip au kwa kutumia Docker.

Slither kupitia pip:

pip3 install --user slither-analyzer

Slither kupitia Docker:

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/trufflecon trailofbits/eth-security-toolbox

Amri ya mwisho inaendesha eth-security-toolbox kwenye Docker ambayo ina ufikiaji wa saraka yako ya sasa. Unaweza kubadilisha faili kutoka kwa mwenyeji wako, na kuendesha zana kwenye faili kutoka kwa Docker

Ndani ya Docker, endesha:

solc-select 0.5.11
cd /home/trufflecon/

Kuendesha hati

Ili kuendesha hati ya Python na Python 3:

python3 script.py

Mstari wa amri

Mstari wa amri dhidi ya hati zilizofafanuliwa na mtumiaji. Slither inakuja na seti ya vigunduzi vilivyofafanuliwa awali ambavyo hupata hitilafu nyingi za kawaida. Kuita Slither kutoka kwenye mstari wa amri kutaendesha vigunduzi vyote, hakuna ujuzi wa kina wa uchanganuzi tuli unaohitajika:

slither project_paths

Mbali na vigunduzi, Slither ina uwezo wa kukagua msimbo kupitia vichapishaji (inafunguka katika kichupo kipya) na zana (inafunguka katika kichupo kipya) zake.

Tumia crytic.io (inafunguka katika kichupo kipya) kupata ufikiaji wa vigunduzi vya kibinafsi na ujumuishaji wa GitHub.

Uchanganuzi tuli

Uwezo na muundo wa mfumo wa uchanganuzi tuli wa Slither umeelezwa katika machapisho ya blogu (1 (inafunguka katika kichupo kipya), 2 (inafunguka katika kichupo kipya)) na jarida la kitaaluma (inafunguka katika kichupo kipya).

Uchanganuzi tuli upo katika aina tofauti. Kuna uwezekano mkubwa unatambua kuwa vikusanyaji kama clang (inafunguka katika kichupo kipya) na gcc (inafunguka katika kichupo kipya) hutegemea mbinu hizi za utafiti, lakini pia inasaidia (Infer (inafunguka katika kichupo kipya), CodeClimate (inafunguka katika kichupo kipya), FindBugs (inafunguka katika kichupo kipya) na zana zinazotegemea mbinu rasmi kama Frama-C (inafunguka katika kichupo kipya) na Polyspace (inafunguka katika kichupo kipya).

Hatutakuwa tukipitia kwa kina mbinu za uchanganuzi tuli na watafiti hapa. Badala yake, tutazingatia kile kinachohitajika kuelewa jinsi Slither inavyofanya kazi ili uweze kuitumia kwa ufanisi zaidi kupata hitilafu na kuelewa msimbo.

Uwakilishi wa msimbo
Uchanganuzi wa msimbo
Uwakilishi wa kati

Uwakilishi wa msimbo

Tofauti na uchanganuzi thabiti, ambao hutoa sababu kuhusu njia moja ya utekelezaji, uchanganuzi tuli hutoa sababu kuhusu njia zote kwa wakati mmoja. Ili kufanya hivyo, inategemea uwakilishi tofauti wa msimbo. Mbili zinazojulikana zaidi ni mti wa sintaksia dhahania (AST) na grafu ya mtiririko wa udhibiti (CFG).

Miti ya Sintaksia Dhahania (AST)

AST hutumiwa kila wakati kikusanyaji kinapochanganua msimbo. Pengine ni muundo wa kimsingi zaidi ambao uchanganuzi tuli unaweza kufanywa.

Kwa ufupi, AST ni mti uliopangwa ambapo, kwa kawaida, kila jani lina kigezo au mara kwa mara na nodi za ndani ni viendeshaji au shughuli za mtiririko wa udhibiti. Fikiria msimbo ufuatao:

function safeAdd(uint a, uint b) pure internal returns(uint){
    if(a + b <= a){
        revert();
    }
    return a + b;
}

AST inayolingana imeonyeshwa katika:

Slither hutumia AST iliyosafirishwa na solc.

Ingawa ni rahisi kujenga, AST ni muundo uliowekwa. Wakati mwingine, hii sio rahisi zaidi kuchanganua. Kwa mfano, ili kutambua shughuli zinazotumiwa na usemi a + b <= a, lazima kwanza uchanganue <= na kisha +. Mbinu ya kawaida ni kutumia kile kinachoitwa muundo wa mgeni, ambacho hupitia mti kwa kujirudia. Slither ina mgeni wa jumla katika ExpressionVisitor (inafunguka katika kichupo kipya).

Msimbo ufuatao unatumia ExpressionVisitor kugundua ikiwa usemi una nyongeza:

from slither.visitors.expression.expression import ExpressionVisitor
from slither.core.expressions.binary_operation import BinaryOperationType

class HasAddition(ExpressionVisitor):

    def result(self):
        return self._result

    def _post_binary_operation(self, expression):
        if expression.type == BinaryOperationType.ADDITION:
            self._result = True

visitor = HasAddition(expression) # expression ni kielelezo kinachopaswa kujaribiwa
print(f'The expression {expression} has a addition: {visitor.result()}')

Grafu ya Mtiririko wa Udhibiti (CFG)

Uwakilishi wa pili wa msimbo unaojulikana zaidi ni grafu ya mtiririko wa udhibiti (CFG). Kama jina lake linavyopendekeza, ni uwakilishi unaotegemea grafu ambao unafichua njia zote za utekelezaji. Kila nodi ina maagizo moja au mengi. Kingo kwenye grafu zinawakilisha shughuli za mtiririko wa udhibiti (kama/basi/vinginevyo, kitanzi, n.k). CFG ya mfano wetu uliopita ni:

CFG ni uwakilishi ambao juu yake uchanganuzi mwingi hujengwa.

Uwakilishi mwingine mwingi wa msimbo upo. Kila uwakilishi una faida na hasara kulingana na uchanganuzi unaotaka kufanya.

Uchanganuzi

Aina rahisi zaidi ya uchanganuzi unaoweza kufanya na Slither ni uchanganuzi wa kisintaksia.

Uchanganuzi wa sintaksia

Slither inaweza kupitia vipengele tofauti vya msimbo na uwakilishi wao ili kupata kutofautiana na dosari kwa kutumia mbinu inayofanana na kulinganisha muundo.

Kwa mfano vigunduzi vifuatavyo vinatafuta masuala yanayohusiana na sintaksia:

Kufunika kigezo cha hali (inafunguka katika kichupo kipya): hurudia juu ya vigezo vyote vya hali na kuangalia ikiwa yoyote inafunika kigezo kutoka kwa mkataba uliorithiwa (state.py#L51-L62 (inafunguka katika kichupo kipya))
Kiolesura kisicho sahihi cha ERC-20 (inafunguka katika kichupo kipya): tafuta sahihi zisizo sahihi za utendakazi wa ERC-20 (incorrect_erc20_interface.py#L34-L55 (inafunguka katika kichupo kipya))

Uchanganuzi wa kisemantiki

Tofauti na uchanganuzi wa sintaksia, uchanganuzi wa kisemantiki utaenda ndani zaidi na kuchanganua "maana" ya msimbo. Familia hii inajumuisha aina fulani pana za uchanganuzi. Zinasababisha matokeo yenye nguvu na muhimu zaidi, lakini pia ni ngumu zaidi kuandika.

Uchanganuzi wa kisemantiki hutumiwa kwa ugunduzi wa hali ya juu zaidi wa udhaifu.

Uchanganuzi wa utegemezi wa data

Kigezo variable_a inasemekana kuwa inategemea data ya variable_b ikiwa kuna njia ambayo thamani ya variable_a inasukumwa na variable_b.

Katika msimbo ufuatao, variable_a inategemea variable_b:

// ...
variable_a = variable_b + 1;

Slither inakuja na uwezo uliojengewa ndani wa utegemezi wa data (inafunguka katika kichupo kipya), shukrani kwa uwakilishi wake wa kati (uliojadiliwa katika sehemu ya baadaye).

Mfano wa matumizi ya utegemezi wa data unaweza kupatikana katika kigunduzi hatari cha usawa mkali (inafunguka katika kichupo kipya). Hapa Slither itatafuta ulinganisho mkali wa usawa kwa thamani hatari (incorrect_strict_equality.py#L86-L87 (inafunguka katika kichupo kipya)), na itamjulisha mtumiaji kwamba inapaswa kutumia >= au <= badala ya ==, ili kuzuia mshambuliaji kunasa mkataba. Miongoni mwa mengine, kigunduzi kitazingatia kama hatari thamani ya kurudi ya wito kwa balanceOf(address) (incorrect_strict_equality.py#L63-L64 (inafunguka katika kichupo kipya)), na itatumia injini ya utegemezi wa data kufuatilia matumizi yake.

Ukokotoaji wa uhakika uliowekwa

Ikiwa uchanganuzi wako unapitia CFG na kufuata kingo, kuna uwezekano wa kuona nodi zilizotembelewa tayari. Kwa mfano, ikiwa kitanzi kinawasilishwa kama inavyoonyeshwa hapa chini:

for(uint i; i < range; ++){
    variable_a += 1
}

Uchanganuzi wako utahitaji kujua wakati wa kuacha. Kuna mikakati miwili mikuu hapa: (1) kurudia kwenye kila nodi idadi isiyo na kikomo ya nyakati, (2) kukokotoa kile kinachoitwa fixpoint. Fixpoint kimsingi inamaanisha kuwa kuchanganua nodi hii hakutoi habari yoyote ya maana.

Mfano wa fixpoint inayotumiwa inaweza kupatikana katika vigunduzi vya uingiaji upya: Slither inachunguza nodi, na kutafuta simu za nje, kuandika na kusoma kwenye hifadhi. Mara tu inapofikia fixpoint (reentrancy.py#L125-L131 (inafunguka katika kichupo kipya)), inasimamisha uchunguzi, na kuchanganua matokeo ili kuona ikiwa uingiaji upya upo, kupitia mifumo tofauti ya uingiaji upya (reentrancy_benign.py (inafunguka katika kichupo kipya), reentrancy_read_before_write.py (inafunguka katika kichupo kipya), reentrancy_eth.py (inafunguka katika kichupo kipya)).

Kuandika uchanganuzi kwa kutumia ukokotoaji mzuri wa uhakika uliowekwa kunahitaji uelewa mzuri wa jinsi uchanganuzi unavyoeneza habari zake.

Uwakilishi wa kati

Uwakilishi wa kati (IR) ni lugha inayokusudiwa kuwa rahisi zaidi kwa uchanganuzi tuli kuliko ile ya asili. Slither inatafsiri Solidity kwa IR yake yenyewe: SlithIR (inafunguka katika kichupo kipya).

Kuelewa SlithIR sio lazima ikiwa unataka tu kuandika hundi za msingi. Hata hivyo, itakuwa muhimu ikiwa unapanga kuandika uchanganuzi wa hali ya juu wa kisemantiki. Vichapishaji vya SlithIR (inafunguka katika kichupo kipya) na SSA (inafunguka katika kichupo kipya) vitakusaidia kuelewa jinsi msimbo unavyotafsiriwa.

Misingi ya API

Slither ina API inayokuruhusu kuchunguza sifa za msingi za mkataba na utendaji wake.

Ili kupakia msingi wa msimbo:

from slither import Slither
slither = Slither('/path/to/project')

Kuchunguza mikataba na utendaji

Kitu cha Slither kina:

contracts (list(Contract): orodha ya mikataba
contracts_derived (list(Contract): orodha ya mikataba ambayo haijarithiwa na mkataba mwingine (kikundi kidogo cha mikataba)
get_contract_from_name (str): Rudisha mkataba kutoka kwa jina lake

Kitu cha Contract kina:

name (str): Jina la mkataba
functions (list(Function)): Orodha ya utendaji
modifiers (list(Modifier)): Orodha ya utendaji
all_functions_called (list(Function/Modifier)): Orodha ya utendaji wote wa ndani unaoweza kufikiwa na mkataba
inheritance (list(Contract)): Orodha ya mikataba iliyorithiwa
get_function_from_signature (str): Rudisha Utendaji kutoka kwa sahihi yake
get_modifier_from_signature (str): Rudisha Kirekebishaji kutoka kwa sahihi yake
get_state_variable_from_name (str): Rudisha Kigezo cha Hali kutoka kwa jina lake

Kitu cha Function au Modifier kina:

name (str): Jina la utendaji
contract (contract): mkataba ambapo utendaji umetangazwa
nodes (list(Node)): Orodha ya nodi zinazounda CFG ya utendaji/kirekebishaji
entry_point (Node): Sehemu ya kuingia ya CFG
variables_read (list(Variable)): Orodha ya vigezo vilivyosomwa
variables_written (list(Variable)): Orodha ya vigezo vilivyoandikwa
state_variables_read (list(StateVariable)): Orodha ya vigezo vya hali vilivyosomwa (kikundi kidogo cha vigezo vilivyosomwa)
state_variables_written (list(StateVariable)): Orodha ya vigezo vya hali vilivyoandikwa (kikundi kidogo cha vigezo vilivyoandikwa)