In this paper, we introduce a cross-layer modeling and verification system that can analyzes the configurations and policies across both application and network components as a single unit. It combines policies from different devices as firewalls, NAT, routers and IPSec gateways as well as basic RBAC-based policies of higher service layers. This will allow analyzing, for example, firewall polices in the context of application access control and vice versa. Thus, by incorporating policies across the network and over multiple layers, we provide a true end-to-end configuration verification tool. Our model represents the system as a state machine where packet header, service request and location determine the state and transitions that conform with the configurations, device operations, and packet values are established. We encode the model as Boolean functions using binary decision diagrams (BDDs). We used an extended version of computational tree logic (CTL) to provide more useful operators and then use it with symbolic model checking to prove or find counter examples to needed properties. The tool is implemented and we gave special consideration to efficiency and scalability. Our extensive evaluation study shows acceptable computation and space requirements with large number of nodes and configuration sizes.