Security design at architecture level is critical to achieve high assurance software systems. However, most security design techniques for software architectures were in ad hoc fashion and fell short in precise notations. This paper proposes a formal aspect-oriented approach to designing secure software architectures. The underlying formalism is the Software Architecture Model (SAM) that combines Petri nets and temporal logic. SAM supports a precise way to model the problem domain, its software architecture, and security aspects of the software architecture. An integrated architecture is obtained by weaving aspect models with the base architecture model. Mechanisms in SAM are amenable to analyzing correctness of the architecture design.