隨機(jī)數(shù)發(fā)生器的安全性證明技術(shù)研究.pdf

1、從1965年4月摩爾在《電子學(xué)》雜志上的一篇文章中提出摩爾定律的半個(gè)多世紀(jì)以來(lái)，半導(dǎo)體發(fā)展迅速。集成電路已經(jīng)應(yīng)用到各個(gè)領(lǐng)域，無(wú)處不在，手機(jī)、電腦等數(shù)字產(chǎn)品深入每個(gè)人的生活，成為人們生活不可或缺的產(chǎn)品。因此集成電路的安全性越來(lái)越受到重視。
　　隨著集成電路技術(shù)的不斷發(fā)展，為了適應(yīng)市場(chǎng)，降低電路的設(shè)計(jì)成本和研發(fā)周期，SoC開(kāi)發(fā)已經(jīng)成為集成電路的設(shè)計(jì)主流。IP庫(kù)是SoC設(shè)計(jì)的重要組成部分，在使用第三方IP庫(kù)的時(shí)候安全性也成為了一個(gè)突出的

2、問(wèn)題。集成電路的設(shè)計(jì)和制造分離，工廠遷往勞動(dòng)力成本低的地區(qū)，不少設(shè)計(jì)也外包給了其他設(shè)計(jì)公司，在集成電路的設(shè)計(jì)過(guò)程中會(huì)使用到各種不同公司提供的電子設(shè)計(jì)自動(dòng)化軟件，因此現(xiàn)在的半導(dǎo)體芯片在設(shè)計(jì)過(guò)程中變得比以前更容易受到惡意篡改。
　　針對(duì)這個(gè)問(wèn)題本文采用Coq來(lái)進(jìn)行電路的安全性證明（等價(jià)安全性）。Coq是一種定理證明軟件，適合于定理的正確性驗(yàn)證。本文先用Coq構(gòu)建隨機(jī)數(shù)發(fā)生器后處理算法的RTL代碼的模型，然后將電路的RTL代碼用這個(gè)模型