Abstract
We present ParTypes, a type-based methodology for the verification of Message Passing Interface (MPI) programs written in the C programming language. The aim is to statically verify programs against protocol specifications, enforcing properties such as fidelity and absence of deadlocks. We develop a protocol language based on a dependent type system for message-passing parallel programs, which includes various communication operators, such as point-to-point messages, broadcast, reduce, array scatter and gather. For the verification of a program against a given protocol, the protocol is first translated into a representation read by VCC, a software verifier for C. We successfully verified several MPI programs in a running time that is independent of the number of processes or other input parameters. This contrasts with alternative techniques, notably model checking and runtime verification, that suffer from the state-explosion problem or that otherwise depend on parameters to the program itself. We experimentally evaluated our approach against state-of-the-art tools for MPI to conclude that our approach offers a scalable solution.

Abstract
Uncoordinated Frequency Hopping (UFH) has been proposed as a mechanism to address denial-of-service attacks, and consists of legitimate devices hopping uniformly at random between frequencies to cope with an attacker that aims to disrupt communication. We consider the use of UFH against an eavesdropper adversary that aims to overhear as much information as possible. We characterize the secrecy level of wireless networks under UFH, showing the harmful security effect of broadband eavesdropper adversaries capable of overhearing in multiple frequencies. To counter such eavesdroppers, we consider the use of broadband friendly jammers that are available to cause interference on eavesdroppers. Our results show that adding a limited number of broadband friendly jammers effectively improves the security level of such systems.

Abstract
Uncoordinated Frequency Hopping (UFH) has been proposed as a mechanism to address denial-of-service attacks, and consists of legitimate devices hopping uniformly at random between frequencies to cope with an attacker that aims to disrupt communication. We consider the use of UFH against an eavesdropper adversary that aims to overhear as much information as possible. We characterize the secrecy level of wireless networks under UFH, showing the harmful security effect of broadband eavesdropper adversaries capable of overhearing in multiple frequencies. To counter such eavesdroppers, we consider the use of broadband friendly jammers that are available to cause interference on eavesdroppers. Our results show that adding a limited number of broadband friendly jammers effectively improves the security level of such systems. © 2015 IEEE.

Abstract
Most of current physical-layer security techniques rely on a degraded eavesdropper, thus warranting some sort of advantage that can be relied upon to achieve higher levels of security. We consider instead non-degraded eavesdroppers, that possess equal or better capabilities than legitimate receivers. Under this challenging setup, most of current physical-layer security techniques become hard to administer and new dimensions to establish advantageous periods of communication are needed. For that, we characterize the secrecy level of two schemes for physical-layer security under non-degraded eavesdroppers: a spread spectrum uncoordinated frequency hopping scheme, and a jamming receiver with self-interference cancellation.

Abstract
We propose a coding scheme based on the combination of interleaving with systematic channel codes for secrecy. The basic idea consists of generating a random interleaving key that is used to shuffle/interleave information at the source. The message and the interleaving key are then both encoded with a systematic code and the part related to the interleaving key is removed/punctured before being sent to the channel, hence operating as a hidden key for any receiver (legitimate or not) that needs to deinterleave the message. Successfully obtaining the original message then depends on determining the interleaving key, which can only be done through the parity bits that result from jointly encoding the interleaving key and the message. We provide a method to determine the necessary signal-to-noise ratio difference that enables successful reception at the legitimate receiver without the eavesdropper having access to the message. In addition, we provide evidence that this scheme may also be used to turn a realistic channel into a discrete memoryless channel, thus providing a first practical implementation of an abstract channel that can be employed with a wiretap code to provide information-theoretic security guarantees. © 2015 IEEE.

Abstract
We propose a coding scheme based on the combination of interleaving with systematic channel codes for secrecy. The basic idea consists of generating a random interleaving key that is used to shuffle/interleave information at the source. The message and the interleaving key are then both encoded with a systematic code and the part related to the interleaving key is removed/punctured before being sent to the channel, hence operating as a hidden key for any receiver (legitimate or not) that needs to deinterleave the message. Successfully obtaining the original message then depends on determining the interleaving key, which can only be done through the parity bits that result from jointly encoding the interleaving key and the message. We provide a method to determine the necessary signal-to-noise ratio difference that enables successful reception at the legitimate receiver without the eavesdropper having access to the message. In addition, we provide evidence that this scheme may also be used to turn a realistic channel into a discrete memoryless channel, thus providing a first practical implementation of an abstract channel that can be employed with a wiretap code to provide information-theoretic security guarantees.