While existing solutions can provide authentication services, they are insufficient for a new generation of network coding-based reprogramming protocols in wireless sensor networks. We present a security approach that is able to defend pollution attack against reprogramming protocols based on network coding. It employs a homomorphic hashing function and an identity-based aggregate signature to allow sensor nodes to check packets on-the-fly before they accept incoming encoded packets, and introduces an efficient mechanism to reduce the computation overhead at each node and to eliminate bad packets quickly. Castalia simulations show that when the 5% of the nodes in a network of 100 nodes are rogue, using our approach, the efficiency of the secure reprogramming protocol based on network coding improves almost ten-fold for a checking probability of 2%.

Reprogramming protocols provide a convenient way to update program images via wireless communication.
In hostile environments where there may be malicious attacks against wireless sensor networks, the process of reprogramming faces threats from potentially compromised nodes. While existing solutions can provide authentication services, they are insufficient for a new generation of network coding-based reprogramming protocols in wireless sensor networks. We present a security approach that is able to defend pollution attack against reprogramming protocols based on network coding. It employs a homomorphic hashing function and an identity-based aggregate signature to allow sensor nodes to check packets on-the-fly before they accept incoming encoded packets, and introduces an efficient mechanism to reduce the computation overhead at each node and to eliminate bad packets quickly. Castalia simulations show that when the 5% of the nodes in a network of 100 nodes are rogue, using our approach, the efficiency of the secure reprogramming protocol based on network coding improves almost ten-fold for a checking probability of 2%.

Considering that cold-chain involves lots of complicated operations which suffer from various uncertain factors during the process of implementing, it is inevitable to establish a sound and detailed risk assessment principle or means to guarantee the safety of cold-chain. HACCP, Hazard Analysis and Critical Control Point, is chosen to be a useful tool to analyze the processes of cold-chain, assess the potential risks for each operation link, and then identify the critical control points and give the appropriate risk weights, so as to ensure the safety, quality and reliability of the cold-chain.

With the increasing pressure on non-function attributes (security, safety and reliability) requirements of an operation system, high–confidence operation system is becoming more important. Formal verification is the only known way to guarantee that a system is free of programming errors. We research on formal verification of operation system kernel in system code level and take theorem proving and model checking as the main technical methods to resolve the key techniques of verifying operation system kernel in C code level. We present a case study to the verification of real-world C systems code derived from an implementation of μC/OS – II in the end.