3備用-12589-C-rusted_EWChina23.pdf

1、A seamless revolution for the safe use of the language family that has passed the test of timeC is a critical infrastructure of the worldC is supported by strong economic reasons270002500023000210001900017000150002018 2019 2020 2021 2022If used without discipline C has great safety and security issu

2、es MISRA compliance solves many of these but not allThe industry is so concerned about these issues that a passage to Rust is actually being discussedWhat if there was a safer and cheaper way?In short,the borrow checker and much more can be implemented for C,yet preserving the entire C ecosystem (an

3、d the huge investments done on it)In fact there is!1void process(char*string);23int foo(const char*fname,size_t bufsize)4int fd=open(fname,O_RDONLY);5char*buf=(char*)malloc(bufsize);6+fd;7ssize_t bytes=read(fd,buf,bufsize-1U);8bufbytes=0;9process(buf);10return 0;11No Warnings by the CompilerSeveral

4、Warnings by the C-rusted Analyzer1#include 23void process(char*e hown string);45int foo(const char*fname,size_t bufsize)6int fd=open(fname,O_RDONLY);7if(fd=-1)return 1;8char*buf=(char*)malloc(bufsize);9if(buf=NULL|bufsize=0U)return 1;10ssize_t bytes=read(fd,buf,bufsize-1U);11if(bytes=-1)12free(buf);

5、13return 1;1415bufbytes=0;16process(buf);17return(close(fd)=-1)?1:0;18No Warnings by the C-rusted Analyzer1typedef inte type()e geq(0)fd_t;2typedef fd_te own(fd)own_fd_t;3typedef own_fd_t e opt(-1)opt_own_fd_t;45/Read property.6opt_own_fd_t e with(r)7open(const char*path,8int e and eq(O RDONLY|O WRO

6、NLY|O RDWR,O RDONLY)oflag);910/Write property.11opt_own_fd_t e with(w)12open(const char*path,13int e and eq(O RDONLY|O WRONLY|O RDWR,O WRONLY)oflag);1415/Read and write properties.16opt_own_fd_t e with(r,w)17open(const char*path,18int e and eq(O RDONLY|O WRONLY|O RDWR,O RDWR)oflag);Standard Librarie

7、s Come Preannotated1typedef fd_t e shar()shar_fd_t;23ssize_t e geq(-1)4read(shar_fd_t e with(r)fildes,5void*buf,size_t nbyte);67ssize_t e geq(-1)8write(shar_fd_t e with(w)filedes,9const void*buf,size_t nbyte);1011int e range(-1,0)12close(own_fd_t filedes);1314int foo(shar_fd_t e with(r,w)filedes,15c

8、har*buf,size_t nbyte)16int res1=read(filedes,buf,nbyte);17int res2=write(filedes,Hellon,6U);18return(res1=-1|res2=-1)?1:0;19Standard Libraries Come Preannotated(contd)1#include 23typedef double e type()e geq(-273.15)celsius_t;4typedef double e type()e geq(0)kelvin_t;5typedef double e type()dltcelsiu

9、s_t;6typedef double e type()dltkelvin_t;78e bop(dltcelsius t,-,celsius t,celsius t);9e bop(dltkelvin t,-,kelvin t,kelvin t);10e bop(double,/,kelvin t,kelvin t);1112void foo(void)13/.14dltcelsius_t dltc=c1-c2;15double c_ratio=c1/c2;16double k_ratio=k1/k2;17Nominal Typing1#include 23typedef double e t

10、ype()volt_t;4typedef double e type()ohm_t;5typedef double e type()ampere_t;67e bop(volt t,*,ampere t,ohm t);8e bop(volt t,*,ohm t,ampere t);910volt_t get_voltage(ampere_t i,ohm_t r)11return i*r;12Nominal Typing(contd)1#include 23#define e opt shar e opt(0)e shar()4#define e opt excl e opt(0)e excl()

11、56typedef struct 7int elem;8struct List_t*e opt hown next;9 List_t;1011void list_print(const List_t*e opt shar p);12bool list_insert(List_t*e opt excl p,int elem);13void list_free(List_t*e opt hown p);Exclusive and Shared Handles1#include 23typedef struct /*.*/T;45T*foo(void)6T t;7/.8return&t;91011T

12、*fie(T*p)12/.13return p;14Implicit Regions1#include 23int*e region(r2)4foo(int*e region(r1)p1,int*e region(r2)p2)5/.6return p2;789void fie(void)10int x=5;11int*res;1213int y=7;14res=foo(&x,&y);1516*res=42;17Explicit Regions1#include 23typedef struct /*.*/e fini()Channel_t;45void channel_ctor(Channel

13、_t e init()*p_chan);6bool channel_send(Channel_t*p_chan,const char*msg);7void channel_dtor(Channel_t e fini()*p_chan);89int foo(void)10Channel_t c;11channel_send(&c,.);12channel_ctor(&c);13if(!channel_send(&c,Message)return-1;14channel_dtor(&c);15return 0;16Resource Management1#include 23typedef str

14、uct Mixer Mixer_t;45void mixer_open(Mixer_t e in(blade=off)e out(door=opened)*p_mx);6void mixer_close(Mixer_t e out(door=closed)*p_mx);7void mixer_on(Mixer_t e in(door=closed)e out(blade=on)*p_mx);8void mixer_off(Mixer_t e out(blade=off)*p_mx);910void foo(Mixer_t e in(blade=off)e out(door=?)*p_mx)11

15、mixer_on(p mx);/Door may be open!12mixer_close(p_mx);13/Door closed.14mixer_on(p_mx);15/Blade on.16return;/Blade still on!17Resource Management(contd)Static Analysis within the C-rusted Analyzer Rigorously intra-procedural Semantics of functions captured(to the required extent)by explicit and implic

16、it annotations Ensures scalability,incrementality and modularity1int iabs(int x)2return x=0?x:-x;3Intermediate Form(Not LLVM,despite the front-end is a derivative of Clang)ECLAIR own intermediate form especially tailoredto static analysis1BB1():2stack_address(V1,x)3get_arg(V2)4write(V1,V2)5read(V3,V

17、1)6constant(V4,0)7ge(V5,V3,V4)89BB2()pred(BB1,if(V5,1):1011BB3()pred(BB1,if(V5,0):12minus(V6,V3)1314BB4(V7)pred(BB2,value(V3)pred(BB3,value(V6):15set_return(V7)Intermediate Form(contd)Points-To AnalysisPath-sensitive,stack-based analysis defined by Maryam Emami(McGill University Montreal):intra-proc

18、edural only rather sophisticated filters(missing in the original)heap-based analysis unnecessary:abstract locationscorresponding to C-rusted regions are used insteadof heap abstractionsOther AnalysesLiveness analysisValue range analysis based on constraint propagationover multi-intervals:integers fl

19、oating-point numbers(including the math library)WIP:special domain(also based on intervals)for the more precise tracking of bitwise operationsuninitreadablepauseddeadfinalizedreleasedinitreleaserdwrfinikillpausereleaseinitfinireleaseresumeinitfinireleaseinitreleaseC-rusted-specific Finite DomainsCha

20、llenges and Opportunities for the C-rusted Analyzer Speed of the analysis Predictability of the analysis Combination with other analysesCC-rustedRustStandardizedYes:ISOYes:it is ISO CNo:moving targetCertifiable translators existYesYes:it is ISO CNoPortabilityAbsoluteAbsoluteLimitedTool availabilityV

21、ery largeVery largeScarceDevelopers availabilityLargeLargeScarceCoding standards for safety and securityYesYesNoCan reuse C legacy codeYesOnly in some casesStrong guarantees on memory resources for annotated programsYesYesStrong guarantees on user-defined resources for annotated programsYesYesCompat

22、ibility with unannotated codeYesYesIncremental adoptionYesNoCost of retraining C programmers for unannotated codeZeroSignificantCost of retraining C programmers for annotated codeModerateSignificantC-rusted:The Advantages of Rust,in C,without the DisadvantagesC-rusted Roadmap A book on the full lang

23、uage definition will be published in Q3 2023 The implementation of the C-rusted Analyzer within the ECLAIR Software Verification Platform is currently under alpha testing An extensive campaign of beta testing and early adoption will follow It will be released with ECLAIR 3.14.0,and will be certified by TV SD according to IEC 61508:2010 up to SIL 4,ISO 26262:2018 up to ASIL D,EN 50128:2011+A2:2020 up to SIL 4,EN 50657:2017 up to SIL 4,IEC 62304:2006+Amd 1:2015 up to Class C,ISO 25119:2018+Amd 1:2020 up to SRL 3,and ISO 19014:2018 up to MPLr e