With the wide application of electronic hardware in aircraft such as air-to-ground communication,satellite communication,positioning system and so on,aircraft hardware is facing great secure pressure.Focusing on the s...With the wide application of electronic hardware in aircraft such as air-to-ground communication,satellite communication,positioning system and so on,aircraft hardware is facing great secure pressure.Focusing on the secure problem of aircraft hardware,this paper proposes a supervisory control architecture based on secure System-on-a-Chip(So C)system.The proposed architecture is attack-immune and trustworthy,which can support trusted escrow application and Dynamic Integrity Measurement(DIM)without interference.This architecture is characterized by a Trusted Monitoring System(TMS)hardware isolated from the Main Processor System(MPS),a secure access channel from TMS to the running memory of the MPS,and the channel is unidirectional.Based on this architecture,the DIM program running on TMS is used to measure and call the Lightweight Measurement Agent(LMA)program running on MPS.By this method,the Operating System(OS)kernel,key software and data of the MPS can be dynamically measured without disturbance,which makes it difficult for adversaries to attack through software.Besides,this architecture has been fully verified on FPGA prototype system.Compared with the existing systems,our architecture achieves higher security and is more efficient on DIM,which can fully supervise the running of application and aircraft hardware OS.展开更多
It is often the case that in the development of a system-on-a-chip(SoC)design,a family of SystemC transaction level models(TLM)is created.TLMs in the same family often share common functionalities but differ in their ...It is often the case that in the development of a system-on-a-chip(SoC)design,a family of SystemC transaction level models(TLM)is created.TLMs in the same family often share common functionalities but differ in their timing,implementation,configuration and performance in various SoC developing phases.In most cases,all the TLMs in a family must be verified for the follow-up design activities.In our previous work,we proposed to call such family TLM product line(TPL),and proposed feature-oriented(FO)design methodology for efficient TPL development.However,developers can only verify TLM in a family one by one,which causes large portion of duplicated verification overhead.Therefore,in our proposed methodology,functional verification of TPL has become a bottleneck.In this paper,we proposed a novel TPL verification method for FO designs.In our method,for the given property,we can exponentially reduce the number of TLMs to be verified by identifying mutefeature-modules(MFM),which will avoid duplicated veri-fication.The proposed method is presented in informal and formal way,and the correctness of it is proved.The theoretical analysis and experimental results on a real design show the correctness and efficiency of the proposed method.展开更多
基金supported by the National Key Research and Development Program of China(No.2017YFB0802502)by the Aeronautical Science Foundation(No.2017ZC51038)+4 种基金by the National Natural Science Foundation of China(Nos.62002006,61702028,61672083,61370190,61772538,61532021,61472429,and 61402029)by the Foundation of Science and Technology on Information Assurance Laboratory(No.1421120305162112006)by the National Cryptography Development Fund(No.MMJJ20170106)by the Defense Industrial Technology Development Program(No.JCKY2016204A102)by the Liaoning Collaboration Innovation Center For CSLE,China。
文摘With the wide application of electronic hardware in aircraft such as air-to-ground communication,satellite communication,positioning system and so on,aircraft hardware is facing great secure pressure.Focusing on the secure problem of aircraft hardware,this paper proposes a supervisory control architecture based on secure System-on-a-Chip(So C)system.The proposed architecture is attack-immune and trustworthy,which can support trusted escrow application and Dynamic Integrity Measurement(DIM)without interference.This architecture is characterized by a Trusted Monitoring System(TMS)hardware isolated from the Main Processor System(MPS),a secure access channel from TMS to the running memory of the MPS,and the channel is unidirectional.Based on this architecture,the DIM program running on TMS is used to measure and call the Lightweight Measurement Agent(LMA)program running on MPS.By this method,the Operating System(OS)kernel,key software and data of the MPS can be dynamically measured without disturbance,which makes it difficult for adversaries to attack through software.Besides,this architecture has been fully verified on FPGA prototype system.Compared with the existing systems,our architecture achieves higher security and is more efficient on DIM,which can fully supervise the running of application and aircraft hardware OS.
基金The work was supported by the National Key R&D Program of China(2018YFB1004202)by Laboratory of Software Engineering for Complex Systems.
文摘It is often the case that in the development of a system-on-a-chip(SoC)design,a family of SystemC transaction level models(TLM)is created.TLMs in the same family often share common functionalities but differ in their timing,implementation,configuration and performance in various SoC developing phases.In most cases,all the TLMs in a family must be verified for the follow-up design activities.In our previous work,we proposed to call such family TLM product line(TPL),and proposed feature-oriented(FO)design methodology for efficient TPL development.However,developers can only verify TLM in a family one by one,which causes large portion of duplicated verification overhead.Therefore,in our proposed methodology,functional verification of TPL has become a bottleneck.In this paper,we proposed a novel TPL verification method for FO designs.In our method,for the given property,we can exponentially reduce the number of TLMs to be verified by identifying mutefeature-modules(MFM),which will avoid duplicated veri-fication.The proposed method is presented in informal and formal way,and the correctness of it is proved.The theoretical analysis and experimental results on a real design show the correctness and efficiency of the proposed method.
