  Our work focuses on modeling security of systems from their component-level
designs. Towards this goal we develop a categorical formalism to model attacker
actions. Equipping the categorical formalism with algebras produces two
interesting results for security modeling. First, using the Yoneda lemma, we
are able to model attacker reconnaissance missions. In this context, the Yoneda
lemma formally shows us that if two system representations, one being complete
and the other being the attacker's incomplete view, agree at every possible
test, then they behave the same. The implication is that attackers can still
successfully exploit the system even with incomplete information. Second, we
model the possible changes that can occur to the system via an exploit. An
exploit either manipulates the interactions between system components, for
example, providing the wrong values to a sensor, or changes the components
themselves, for example, manipulating the firmware of a global positioning
system (GPS). One additional benefit of using category theory is that
mathematical operations can be represented as formal diagrams, which is useful
for applying this analysis in a model-based design setting. We illustrate this
modeling framework using a cyber-physical system model of an unmanned aerial
vehicle (UAV). We demonstrate and model two types of attacks (1) a rewiring
attack, which violates data integrity, and (2) a rewriting attack, which
violates availability.
