Refinement modeling and verification of secure operating systems for communication in digital twins

In traditional digital twin communication system testing,we can apply test cases as completely as possible in order to ensure the correctness of the system implementation,and even then,there is no guarantee that the digital twin communication system implementation is completely correct.Formal verification is currently recognized as a method to ensure the correctness of software system for communication in digital twins because it uses rigorous mathematical methods to verify the correctness of systems for communication in digital twins and can effectively help system designers determine whether the system is designed and implemented correctly.In this paper,we use the interactive theorem proving tool Isabelle/HOL to construct the formal model of the X86 architecture,and to model the related assembly instructions.The verification result shows that the system states obtained after the operations of relevant assembly instructions is consistent with the expected states,indicating that the system meets the design expectations.

Statistically Extrapolated Nowcasting of Summertime Precipitation over the Eastern Alps

This paper presents a new multiple linear regression（MLR） approach to updating the hourly, extrapolated precipitation forecasts generated by the INCA（Integrated Nowcasting through Comprehensive Analysis） system for the Eastern Alps.The generalized form of the model approximates the updated precipitation forecast as a linear response to combinations of predictors selected through a backward elimination algorithm from a pool of predictors. The predictors comprise the raw output of the extrapolated precipitation forecast, the latest radar observations, the convective analysis, and the precipitation analysis. For every MLR model, bias and distribution correction procedures are designed to further correct the systematic regression errors. Applications of the MLR models to a verification dataset containing two months of qualified samples,and to one-month gridded data, are performed and evaluated. Generally, MLR yields slight, but definite, improvements in the intensity accuracy of forecasts during the late evening to morning period, and significantly improves the forecasts for large thresholds. The structure-amplitude-location scores, used to evaluate the performance of the MLR approach,based on its simulation of morphological features, indicate that MLR typically reduces the overestimation of amplitudes and generates similar horizontal structures in precipitation patterns and slightly degraded location forecasts, when compared with the extrapolated nowcasting.

FedDAA:a robust federated learning framework to protect privacy and defend against adversarial attack

Federated learning(FL)has emerged to break data-silo and protect clients’privacy in the field of artificial intelligence.However,deep leakage from gradient(DLG)attack can fully reconstruct clients’data from the submitted gradient,which threatens the fundamental privacy of FL.Although cryptology and differential privacy prevent privacy leakage from gradient,they bring negative effect on communication overhead or model performance.Moreover,the original distribution of local gradient has been changed in these schemes,which makes it difficult to defend against adversarial attack.In this paper,we propose a novel federated learning framework with model decomposition,aggregation and assembling(FedDAA),along with a training algorithm,to train federated model,where local gradient is decomposed into multiple blocks and sent to different proxy servers to complete aggregation.To bring better privacy protection performance to FedDAA,an indicator is designed based on image structural similarity to measure privacy leakage under DLG attack and an optimization method is given to protect privacy with the least proxy servers.In addition,we give defense schemes against adversarial attack in FedDAA and design an algorithm to verify the correctness of aggregated results.Experimental results demonstrate that FedDAA can reduce the structural similarity between the reconstructed image and the original image to 0.014 and remain model convergence accuracy as 0.952,thus having the best privacy protection performance and model training effect.More importantly,defense schemes against adversarial attack are compatible with privacy protection in FedDAA and the defense effects are not weaker than those in the traditional FL.Moreover,verification algorithm of aggregation results brings about negligible overhead to FedDAA.

Implementation and verification of different ECC mitigation designs for BRAMs in flash-based FPGAs

Embedded RAM blocks（BRAMs） in field programmable gate arrays（FPGAs） are susceptible to single event effects（SEEs） induced by environmental factors such as cosmic rays, heavy ions, alpha particles and so on. As technology scales, the issue will be more serious. In order to tackle this issue, two different error correcting codes（ECCs）, the shortened Hamming codes and shortened BCH codes, are investigated in this paper. The concrete design methods of the codes are presented. Also, the codes are both implemented in flash-based FPGAs. Finally, the synthesis report and simulation results are presented in the paper. Moreover, heavy-ion experiments are performed,and the experimental results indicate that the error cross-section of the device using the shortened Hamming codes can be reduced by two orders of magnitude compared with the device without mitigation, and no errors are discovered in the experiments for the device using the shortened BCH codes.