  With ever-expanding computation and communication capabilities of modern
embedded platforms, Internet of Things (IoT) technologies enable development of
Reconfigurable Manufacturing Systems---a new generation of highly modularized
industrial equipment suitable for highly-customized manufacturing. Sequential
control in these systems is largely based on discrete events, while their
formal execution semantics is specified as Control Interpreted Petri Nets
(CIPN). Despite industry-wide use of programming languages based on the CIPN
formalism, formal verification of such control applications in the presence of
adversarial activity is not supported. Consequently, in this paper we focus on
security-aware modeling and verification challenges for CIPN-based sequential
control applications. Specifically, we show how CIPN models of networked
industrial IoT controllers can be transformed into Time Petri Net (TPN)-based
models, and composed with plant and security-aware channel models in order to
enable system-level verification of safety properties in the presence of
network-based attacks. Additionally, we introduce realistic channel-specific
attack models that capture adversarial behavior using nondeterminism. Moreover,
we show how verification results can be utilized to introduce security patches
and motivate design of attack detectors that improve overall system resiliency,
and allow satisfaction of critical safety properties. Finally, we evaluate our
framework on an industrial case study.
