This paper focuses on a new attack vector in modern processors: the timing-based side and covert channel attacks due to the Translation Look-aside Buffers (TLBs). This paper first presents a novel three-step modeling approach that is used to exhaustively enumerate all possible TLB timing-based vulnerabilities. Building on the three-step model, this paper then shows how to automatically generate micro security benchmarks that test for the TLB vulnerabilities. After showing the insecurity of standard TLBs, two new secure TLB designs are presented: a Static-Partition (SP) TLB and a Random-Fill (RF) TLB. The new secure TLBs are evaluated using the Rocket Core implementation of the RISC-V processor architecture enhanced with the two new designs. The three-step model and the security benchmarks are used to analyze the security of the new designs in simulation. Based on the analysis, the proposed secure TLBs can defend not only against the previously publicized attacks but also against other new timing-based attacks in TLBs found using the new three-step model. The performance overhead is evaluated on an FPGA-based setup, and, for example, shows that the RF TLB has less than 10% overhead while defending all the attacks.