This paper studies the embedding and synthesis of knowledge in tree ensemble classifiers. We focus on knowledge expressible with a generic form of Boolean formulas, and show that a typical security attack, i.e., backdoor attack, is expressible with this knowledge expression. For the embedding, it is required to be preservative (i.e., the original performance of the classifier is preserved), verifiable (i.e., the knowledge can be attested), and stealthy (i.e., the embedding cannot be easily detected). To facilitate this, we propose two novel, and very effective, embedding algorithms, one of which is for black-box setting and the other for white-box setting. The embedding can be done in PTIME. Beyond the embedding, we develop an algorithm to synthesise the embedded knowledge, by reducing the problem to be solvable with an SMT (satisfiability modulo theories) solver. While this novel algorithmcan successfully synthesise knowledge, the reduction leads to an NP computation. Therefore, if applying embedding as security attack and synthesis as defence, our results suggest acomplexity gap (P vs. NP) between security attack and security defence when working with machine learning models. We apply our algorithms to a diverse set of datasets to validate our conclusion empirically.