model checking one million lines of c code检查c代码一百万行模型

1,Model Checking One Million Lines of C Code,Hao Chen, UC BerkeleyDrew Dean, SRI InternationalDavid Wagner, UC Berkeley,2,MOPS (MOdel checking Programs for Security properties),A static analysis tool that checks source programs for temporal safety properties.e.g. a setuid-root program must drop privilege before making risky system calls.AnalysisPushdown model checkingInter-proceduralControl flow centric,3,The MOPS process,Parser,ModelChecker,C Program,SafetyProperty,CFG,FSA,Program satisifessafety property,Error Traces,FSA: finite state automatonCFG: control flow graph,Treat the model checker as a black box for this talk,4,Is software model checking readyfor prime time?,Can model checking be used by open source developers to find security vulnerabilities?Criteria for a successful toolIt is usefulCan check many propertiesCan check diverse, widely-deployed programsRequires moderate computational resourcesIt is usableCan be used easily by non-tool developersCan generate comprehensible error reports,5,Outline,ExperimentPrograms: 8 widely-deployed programs, with over 1 million LOCProperties: 5 security-related propertiesFindingsMore than a dozen vulnerabilities and weaknesses Usability improvementsConclusion,6,Programs,7,Security properties,Drop privilege completely when neededAvoid stderr vulnerability Avoid race condition (TOCTTOU)Create chroot-jail safelychdir(“/”) must follow chroot() immediatelyCreate temporary files safelyUse only the safe function mkstemp()Never reuse filename in mkstemp(filename),8,Property: drop privilege completely,Setuid-root programs should drop root privilege completelybefore executing an untrusted program via system(), popen(), execvp() and friends, orwhen the program intends to do soOtherwise, the remaining privilege may be exploited bythe untrusted program that is executedmalicious code injected via buffer overrun attacks,9,Vulnerability: fail to drop privilege completely,seteuid(getuid();setuid(getuid();execlp(askpass, askpass, msg, (char *) 0);,OpenSSH client(in readpass.c),10,What is wrong?,R0, E=S=0,OpenSSH 3.5 on Linux,R=E0, S=0,R=E0, S=0,seteuid(getuid(),setuid(getuid(),R0, E=S=0,OpenSSH 3.5 on OpenBSD,R=E0, S=0,R=E=S0,seteuid(getuid(),setuid(getuid(),R0, E=S=0,OpenSSH 2.5.2 on Linux,R=E=S0,setuid(getuid(),11,Potential Vulnerability,Weaknessesssh: fails to drop privilege before executing a user programssh-keysign: fails to drop privilege before doing complex cryptographic operationsA buffer overrun would allow the attacker to regain root privilege in euid.,12,Property: drop privilege completely,13,Vulnerability: stderr exploits in at,attack.c,at.c,Code,Standard File Descriptorsstdinstdoutstderr,close(1); close(2);,execl(“at”, );,open(LFILE, O_WRONLY);,fd = open(atfile, O_CREAT);,ttyttytty,tty ,tty ,ttyLFILE,ttyLFILEatfile,Rule: No setuid-root program may open a file for writing to stderr,14,Property: stderr vulnerability,15,Summary of Findings,16,Outline,ExperimentPrograms: 8 widely-deployed programs, with over 1 million LOCProperties: 5 security-related propertiesFindingsMore than a dozen vulnerabilities and weaknesses Usability improvementsConclusion,17,Usability improvement 1:Make it really easy to run!,ProblemsPackages have different build processesTool has to be manually configured for each packageSolutionProvide a script that integrates model checking into the build processes of packages automaticallyResult: allow the user to run the tool as simple asmops m setuid.fsa openssh-3.5p1-6.src.rpm,18,Integrating MOPS intoSoftware Build Processes,1st attempt: manually edit MakefilesToo complicated; does not survive autoconf2nd attempt: setenv GCC_EXEC_PREFIX to run MOPS instead of gccBuild processes generate links to object files broken4th attempt: Put CFGs into ELF filesSolves all identified problems!,19,Usability improvement 2:report comprehensible error messages,ProblemOne bug may trigger many error tracesThe user has to review all the traces manuallyCriteria for good error trace reportingReporting one error trace per bugReporting shortest error traces,20,Algorithm,Find the shortest error trace t and output itFind the crucial statement s on t, i.e. the first statement that causes an error on tPrune s from the programIf the program still has error traces, go to step 1,21,Criteria for good tools: revisited,It is usefulCan check many propertiesCan check diverse, widely-deployed programsRequires moderate computational resourcesIt is usableCan be used easily by non-tool developersCan generate comprehensible error reports,22,Conclusion,Mod